1  /-
  2  Copyright (c) 2014 Jeremy Avigad. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Jeremy Avigad, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
  5  
  6  -- QUESTION: can make the first argument in ∀ x ∈ a, ... implicit?
  7  -/
  8  import logic.basic data.set.basic data.equiv.basic
src         └─────────┘ └────────────┘ └──────────────┘
  9  import order.complete_boolean_algebra category.basic
src         └────────────────────────────┘ └────────────┘
 10  import tactic.finish data.sigma.basic order.galois_connection
src         └───────────┘ └──────────────┘ └─────────────────────┘
 11  
 12  open function tactic set lattice auto
 13  
 14  universes u v w x y
 15  variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {ι' : Sort y}
 16  
 17  namespace set
 18  
 19  instance lattice_set : complete_lattice (set α) :=
id                          └──────────────┘  └─┘ 
src                         └──────────────┘  └─┘
typ                         └──────────────┘  └─┘ 
doc                         └──────────────┘
 20  { le     := (⊆),
id               
src              
typ              
 21    lt     := (⊂),
id               
src              
typ              
 22    sup    := (∪),
id               
src              
typ              
 23    inf    := (∩),
id               
src              
typ              
 24    top    := univ,
id               └──┘
src              └──┘
typ              └──┘
 25    bot    := ∅,
id               
src              
typ              
 26    Sup    := λs, {a | ∃ t ∈ s, a ∈ t },
id                            
src                               
typ                           
 27    Inf    := λs, {a | ∀ t ∈ s, a ∈ t },
id                              
src                                
typ                             
 28  
 29    le_Sup := assume s t t_in a a_in, ⟨t, ⟨t_in, a_in⟩⟩,
id                        └──┘  └──┘      └──┘  └──┘
typ                       └──┘  └──┘      └──┘  └──┘
 30    Sup_le := assume s t h a ⟨t', ⟨t'_in, a_in⟩⟩, h t' t'_in a_in,
id                          └┘   └───┘  └──┘    
typ                         └┘   └───┘  └──┘    
 31  
 32    le_Inf := assume s t h a a_in t' t'_in, h t' t'_in a_in,
id                          └──┘ └┘ └───┘   └┘ └───┘ └──┘
typ                         └──┘ └┘ └───┘   └┘ └───┘ └──┘
 33    Inf_le := assume s t t_in a h, h _ t_in,
id                        └──┘       └──┘
typ                       └──┘       └──┘
 34    .. (infer_instance : complete_lattice (α → Prop)) }
id         └────────────┘   └──────────────┘  
src        └────────────┘   └──────────────┘
typ        └────────────┘   └──────────────┘  
doc        └────────────┘   └──────────────┘
 35  
 36  instance : distrib_lattice (set α) :=
id              └─────────────┘  └─┘ 
src             └─────────────┘  └─┘
typ             └─────────────┘  └─┘ 
doc             └─────────────┘
 37  { le_sup_inf := λ s t u x, or_and_distrib_left.2, ..set.lattice_set }
id                          └─────────────────┘     └─────────────┘
src                             └─────────────────┘     └─────────────┘
typ                         └─────────────────┘     └─────────────┘
 38  
 39  lemma monotone_image {f : α → β} : monotone (image f) :=
id                                    └──────┘  └───┘ 
src                                     └──────┘  └───┘
typ                                   └──────┘  └───┘ 
doc                                     └──────┘
 40  assume s t, assume h : s ⊆ t, image_subset _ h
id                            └──────────┘   
src                               └──────────┘
typ                           └──────────┘   
 41  
 42  theorem monotone_inter [preorder β] {f g : β → set α}
id                           └──────┘             └─┘ 
src                          └──────┘               └─┘
typ                          └──────┘             └─┘ 
 43    (hf : monotone f) (hg : monotone g) : monotone (λx, f x ∩ g x) :=
id           └──────┘         └──────┘     └──────┘         
src          └──────┘          └──────┘      └──────┘          
typ          └──────┘         └──────┘     └──────┘         
doc          └──────┘          └──────┘      └──────┘
 44  assume b₁ b₂ h, inter_subset_inter (hf h) (hg h)
id          └┘ └┘   └────────────────┘  └┘    └┘ 
src                  └────────────────┘
typ         └┘ └┘   └────────────────┘  └┘    └┘ 
 45  
 46  theorem monotone_union [preorder β] {f g : β → set α}
id                           └──────┘             └─┘ 
src                          └──────┘               └─┘
typ                          └──────┘             └─┘ 
 47    (hf : monotone f) (hg : monotone g) : monotone (λx, f x ∪ g x) :=
id           └──────┘         └──────┘     └──────┘         
src          └──────┘          └──────┘      └──────┘          
typ          └──────┘         └──────┘     └──────┘         
doc          └──────┘          └──────┘      └──────┘
 48  assume b₁ b₂ h, union_subset_union (hf h) (hg h)
id          └┘ └┘   └────────────────┘  └┘    └┘ 
src                  └────────────────┘
typ         └┘ └┘   └────────────────┘  └┘    └┘ 
 49  
 50  theorem monotone_set_of [preorder α] {p : α → β → Prop}
id                            └──────┘           
src                           └──────┘
typ                           └──────┘           
 51    (hp : ∀b, monotone (λa, p a b)) : monotone (λa, {b | p a b}) :=
id              └──────┘            └──────┘          
src              └──────┘                └──────┘      
typ             └──────┘            └──────┘          
doc              └──────┘                └──────┘
 52  assume a a' h b, hp b h
id           └┘    └┘  
typ          └┘    └┘  
 53  
 54  section galois_connection
 55  variables {f : α → β}
 56  
 57  protected lemma image_preimage : galois_connection (image f) (preimage f) :=
id                                    └───────────────┘  └───┘    └──────┘ 
src                                   └───────────────┘  └───┘     └──────┘
typ                                   └───────────────┘  └───┘    └──────┘ 
doc                                   └───────────────┘            └──────┘
 58  assume a b, image_subset_iff
id             └──────────────┘
src              └──────────────┘
typ            └──────────────┘
doc              └──────────────┘
 59  
 60  def kern_image (f : α → β) (s : set α) : set β := {y | ∀x, f x = y → x ∈ s}
id                                 └─┘     └─┘                   
src                                  └─┘      └─┘                         
typ                                └─┘     └─┘                   
 61  
 62  protected lemma preimage_kern_image : galois_connection (preimage f) (kern_image f) :=
id                                         └───────────────┘  └──────┘    └────────┘ 
src                                        └───────────────┘  └──────┘     └────────┘
typ                                        └───────────────┘  └──────┘    └────────┘ 
doc                                        └───────────────┘  └──────┘
 63  assume a b,
id           
typ          
 64  ⟨ assume h x hx y hy, have f y ∈ a, from hy.symm ▸ hx, h this,
id              └┘  └┘                 └┘└───┘  └┘   └──┘
src                                            └───┘ 
typ             └┘  └┘                 └┘└───┘  └┘   └──┘
 65    assume h x (hx : f x ∈ a), h hx x rfl⟩
id                           └┘  └─┘
src                                     └─┘
typ                          └┘  └─┘
 66  
 67  end galois_connection
 68  
 69  /- union and intersection over a family of sets indexed by a type -/
 70  
 71  /-- Indexed union of a family of sets -/
 72  @[reducible] def Union (s : ι → set β) : set β := supr s
id                                  └─┘     └─┘     └──┘ 
src                                  └─┘      └─┘      └──┘
typ                                 └─┘     └─┘     └──┘ 
doc    └───────┘                                       └──┘
 73  
 74  /-- Indexed intersection of a family of sets -/
 75  @[reducible] def Inter (s : ι → set β) : set β := infi s
id                                  └─┘     └─┘     └──┘ 
src                                  └─┘      └─┘      └──┘
typ                                 └─┘     └─┘     └──┘ 
doc    └───────┘                                       └──┘
 76  
 77  notation `⋃` binders `, ` r:(scoped f, Union f) := r
id                                          └───┘
src                                         └───┘
typ                                         └───┘
doc                                         └───┘
 78  notation `⋂` binders `, ` r:(scoped f, Inter f) := r
id                                          └───┘
src                                         └───┘
typ                                         └───┘
doc                                         └───┘
 79  
 80  @[simp] theorem mem_Union {x : β} {s : ι → set β} : x ∈ Union s ↔ ∃ i, x ∈ s i :=
id                                            └─┘       └───┘        
src                                             └─┘         └───┘         
typ                                           └─┘       └───┘        
doc    └──┘                                                  └───┘
 81  ⟨assume ⟨t, ⟨⟨a, (t_eq : s a = t)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq.symm ▸ h⟩,
id                                                      └───┘ 
src                                                           └───┘ 
typ                                                     └───┘ 
 82    assume ⟨a, h⟩, ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩
id                           └─┘
src                              └─┘
typ                          └─┘
 83  /- alternative proof: dsimp [Union, supr, Sup]; simp -/
 84    -- TODO: more rewrite rules wrt forall / existentials and logical connectives
 85    -- TODO: also eliminate ∃i, ... ∧ i = t ∧ ...
 86  
 87  @[simp] theorem mem_Inter {x : β} {s : ι → set β} : x ∈ Inter s ↔ ∀ i, x ∈ s i :=
id                                            └─┘       └───┘          
src                                             └─┘         └───┘           
typ                                           └─┘       └───┘          
doc    └──┘                                                  └───┘
 88  ⟨assume (h : ∀a ∈ {a : set β | ∃i, s i = a}, x ∈ a) a, h (s a) ⟨a, rfl⟩,
id                        └─┘                         └─┘
src                        └─┘                                     └─┘
typ                       └─┘                         └─┘
 89    assume h t ⟨a, (eq : s a = t)⟩, eq ▸ h a⟩
id                                 
src                                     
typ                                
 90  
 91  theorem Union_subset {s : ι → set β} {t : set β} (h : ∀ i, s i ⊆ t) : (⋃ i, s i) ⊆ t :=
id                                └─┘        └─┘                          
src                                └─┘         └─┘                                 
typ                               └─┘        └─┘                          
doc                                                                           
 92  -- TODO: should be simpler when sets' order is based on lattices
 93  @supr_le (set β) _ set.lattice_set _ _ h
id    └─────┘  └─┘     └─────────────┘     
src   └─────┘  └─┘      └─────────────┘
typ   └─────┘  └─┘     └─────────────┘     
 94  
 95  theorem Union_subset_iff {s : ι → set β} {t : set β} : (⋃ i, s i) ⊆ t ↔ (∀ i, s i ⊆ t) :=
id                                    └─┘        └─┘                      
src                                    └─┘         └─┘                             
typ                                   └─┘        └─┘                      
doc                                                            
 96  ⟨assume h i, subset.trans (le_supr s _) h, Union_subset⟩
id              └──────────┘  └─────┘       └──────────┘
src               └──────────┘  └─────┘         └──────────┘
typ             └──────────┘  └─────┘       └──────────┘
 97  
 98  theorem mem_Inter_of_mem {x : β} {s : ι → set β} : (∀ i, x ∈ s i) → (x ∈ ⋂ i, s i) :=
id                                           └─┘                       
src                                            └─┘                            
typ                                          └─┘                       
doc                                                                             
 99  mem_Inter.2
id   └───────┘
src  └───────┘
typ  └───────┘
100  
101  theorem subset_Inter {t : set β} {s : ι → set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=
id                             └─┘           └─┘                        
src                            └─┘             └─┘                             
typ                            └─┘           └─┘                        
doc                                                                              
102  -- TODO: should be simpler when sets' order is based on lattices
103  @le_infi (set β) _ set.lattice_set _ _ h
id    └─────┘  └─┘     └─────────────┘     
src   └─────┘  └─┘      └─────────────┘
typ   └─────┘  └─┘     └─────────────┘     
104  
105  theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr
id                                   └─┘                       └─────┘
src                                    └─┘                              └─────┘
typ                                  └─┘                       └─────┘
doc                                                             
106  
107  theorem Inter_subset : ∀ (s : ι → set β) (i : ι), (⋂ i, s i) ⊆ s i := infi_le
id                                   └─┘                       └─────┘
src                                    └─┘                              └─────┘
typ                                  └─┘                       └─────┘
doc                                                       
108  
109  lemma Inter_subset_of_subset {s : ι → set α} {t : set α} (i : ι)
id                                        └─┘        └─┘        
src                                        └─┘         └─┘
typ                                       └─┘        └─┘        
110    (h : s i ⊆ t) : (⋂ i, s i) ⊆ t :=
id                        
src                            
typ                       
doc                       
111  set.subset.trans (set.Inter_subset s i) h
id   └──────────────┘  └──────────────┘    
src  └──────────────┘  └──────────────┘
typ  └──────────────┘  └──────────────┘    
112  
113  lemma Inter_subset_Inter {s t : ι → set α} (h : ∀ i, s i ⊆ t i) :
id                                      └─┘                
src                                      └─┘                  
typ                                     └─┘                
114    (⋂ i, s i) ⊆ (⋂ i, t i) :=
id                
src                 
typ               
doc                  
115  set.subset_Inter $ λ i, set.Inter_subset_of_subset i (h i)
id   └──────────────┘       └────────────────────────┘    
src  └──────────────┘        └────────────────────────┘
typ  └──────────────┘       └────────────────────────┘    
116  
117  lemma Inter_subset_Inter2 {s : ι → set α} {t : ι' → set α} (h : ∀ j, ∃ i, s i ⊆ t j) :
id                                     └─┘        └┘   └─┘                  
src                                     └─┘              └─┘                     
typ                                    └─┘        └┘   └─┘                  
118    (⋂ i, s i) ⊆ (⋂ j, t j) :=
id                
src                 
typ               
doc                  
119  set.subset_Inter $ λ j, let ⟨i, hi⟩ := h j in Inter_subset_of_subset i hi
id   └──────────────┘       └─┘    └┘          └────────────────────┘
src  └──────────────┘                              └────────────────────┘
typ  └──────────────┘       └─┘    └┘          └────────────────────┘
120  
121  theorem Union_const [inhabited ι] (s : set β) : (⋃ i:ι, s) = s :=
id                        └───────┘        └─┘             
src                       └───────┘         └─┘               
typ                       └───────┘        └─┘             
doc                                                       
122  ext $ by simp
id   └─┘
src  └─┘      └────
typ  └─┘      └────
doc           └────
txt           └────
par           └────
pid               
st           └─────
123  
src  
typ  
doc  
txt  
par  
pid  
st   
124  theorem Inter_const [inhabited ι] (s : set β) : (⋂ i:ι, s) = s :=
id                        └───────┘        └─┘             
src                       └───────┘         └─┘               
typ                       └───────┘        └─┘             
doc                                                       
125  ext $ by simp
id   └─┘
src  └─┘      └────
typ  └─┘      └────
doc           └────
txt           └────
par           └────
pid               
st           └─────
126  
src  
typ  
doc  
txt  
par  
pid  
st   
127  @[simp] -- complete_boolean_algebra
doc    └──┘
128  theorem compl_Union (s : ι → set β) : - (⋃ i, s i) = (⋂ i, - s i) :=
id                               └─┘                  
src                               └─┘                     
typ                              └─┘                  
doc                                                        
129  ext (by simp)
id   └─┘
src  └─┘     └──┘
typ  └─┘     └──┘
doc          └──┘
txt          └──┘
par          └──┘
st          └───┘
130  
131  -- classical -- complete_boolean_algebra
132  theorem compl_Inter (s : ι → set β) : -(⋂ i, s i) = (⋃ i, - s i) :=
id                               └─┘                 
src                               └─┘                    
typ                              └─┘                 
doc                                                       
133  ext (λ x, by simp [classical.not_forall])
id   └─┘               └──────────────────┘
src  └─┘          └────┘└──────────────────┘
typ  └─┘         └────┘└──────────────────┘
doc               └────┘                    
txt               └────┘                    
par               └────┘                    
pid                                       
st               └──────────────────────────┘
134  
135  -- classical -- complete_boolean_algebra
136  theorem Union_eq_comp_Inter_comp (s : ι → set β) : (⋃ i, s i) = - (⋂ i, - s i) :=
id                                            └─┘                  
src                                            └─┘                     
typ                                           └─┘                  
doc                                                                     
137  by simp [compl_Inter, compl_compl]
id            └─────────┘  └─────────┘
src     └────┘└─────────┘└┘└─────────┘└─
typ     └────┘└─────────┘└┘└─────────┘└─
doc     └────┘           └┘           └─
txt     └────┘           └┘           └─
par     └────┘           └┘           └─
pid                    └┘           
st     └────────────────────────────────
138  
src  
typ  
doc  
txt  
par  
pid  
st   
139  -- classical -- complete_boolean_algebra
src  ────────────────────────────────────────┘
typ  ────────────────────────────────────────┘
doc  ────────────────────────────────────────┘
txt  ────────────────────────────────────────┘
par  ────────────────────────────────────────┘
pid  ────────────────────────────────────────┘
st   ────────────────────────────────────────┘
140  theorem Inter_eq_comp_Union_comp (s : ι → set β) : (⋂ i, s i) = - (⋃ i, -s i) :=
id                                            └─┘                 
src                                            └─┘                     
typ                                           └─┘                 
doc                                                                     
141  by simp [compl_compl]
id            └─────────┘
src     └────┘└─────────┘└─
typ     └────┘└─────────┘└─
doc     └────┘           └─
txt     └────┘           └─
par     └────┘           └─
pid                    
st     └───────────────────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143  theorem inter_Union (s : set β) (t : ι → set β) :
id                            └─┘           └─┘ 
src                           └─┘             └─┘
typ                           └─┘           └─┘ 
144    s ∩ (⋃ i, t i) = ⋃ i, s ∩ t i :=
id                   
src                      
typ                  
doc                     
145  ext $ by simp
id   └─┘
src  └─┘      └────
typ  └─┘      └────
doc           └────
txt           └────
par           └────
pid               
st           └─────
146  
src  
typ  
doc  
txt  
par  
pid  
st   
147  theorem Union_inter (s : set β) (t : ι → set β) :
id                            └─┘           └─┘ 
src                           └─┘             └─┘
typ                           └─┘           └─┘ 
148    (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
id                   
src                        
typ                  
doc                     
149  ext $ by simp
id   └─┘
src  └─┘      └────
typ  └─┘      └────
doc           └────
txt           └────
par           └────
pid               
st           └─────
150  
src  
typ  
doc  
txt  
par  
pid  
st   
151  theorem Union_union_distrib (s : ι → set β) (t : ι → set β) :
id                                       └─┘           └─┘ 
src                                       └─┘             └─┘
typ                                      └─┘           └─┘ 
152    (⋃ i, s i ∪ t i) = (⋃ i, s i) ∪ (⋃ i, t i) :=
id                          
src                                
typ                         
doc                                   
153  ext $ by simp [exists_or_distrib]
id   └─┘            └───────────────┘
src  └─┘      └────┘└───────────────┘└─
typ  └─┘      └────┘└───────────────┘└─
doc           └────┘                 └─
txt           └────┘                 └─
par           └────┘                 └─
pid                                
st           └─────────────────────────
154  
src  
typ  
doc  
txt  
par  
pid  
st   
155  theorem Inter_inter_distrib (s : ι → set β) (t : ι → set β) :
id                                       └─┘           └─┘ 
src                                       └─┘             └─┘
typ                                      └─┘           └─┘ 
156    (⋂ i, s i ∩ t i) = (⋂ i, s i) ∩ (⋂ i, t i) :=
id                          
src                                
typ                         
doc                                   
157  ext $ by simp [forall_and_distrib]
id   └─┘            └────────────────┘
src  └─┘      └────┘└────────────────┘└─
typ  └─┘      └────┘└────────────────┘└─
doc           └────┘                  └─
txt           └────┘                  └─
par           └────┘                  └─
pid                                 
st           └──────────────────────────
158  
src  
typ  
doc  
txt  
par  
pid  
st   
159  theorem union_Union [inhabited ι] (s : set β) (t : ι → set β) :
id                        └───────┘        └─┘           └─┘ 
src                       └───────┘         └─┘             └─┘
typ                       └───────┘        └─┘           └─┘ 
160    s ∪ (⋃ i, t i) = ⋃ i, s ∪ t i :=
id                   
src                      
typ                  
doc                     
161  by rw [Union_union_distrib, Union_const]
id          └─────────────────┘  └─────────┘
src     └──┘└─────────────────┘└┘└─────────┘└─
typ     └──┘└─────────────────┘└┘└─────────┘└─
doc     └──┘                   └┘           └─
txt     └──┘                   └┘           └─
par     └──┘                   └┘           └─
pid       └┘                   └┘           
st     └──────────────────────┘└───────────┘
162  
src  
typ  
doc  
txt  
par  
pid  
st   
163  theorem Union_union [inhabited ι] (s : set β) (t : ι → set β) :
id                        └───────┘        └─┘           └─┘ 
src                       └───────┘         └─┘             └─┘
typ                       └───────┘        └─┘           └─┘ 
164    (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
id                   
src                        
typ                  
doc                     
165  by rw [Union_union_distrib, Union_const]
id          └─────────────────┘  └─────────┘
src     └──┘└─────────────────┘└┘└─────────┘└─
typ     └──┘└─────────────────┘└┘└─────────┘└─
doc     └──┘                   └┘           └─
txt     └──┘                   └┘           └─
par     └──┘                   └┘           └─
pid       └┘                   └┘           
st     └──────────────────────┘└───────────┘
166  
src  
typ  
doc  
txt  
par  
pid  
st   
167  theorem inter_Inter [inhabited ι] (s : set β) (t : ι → set β) :
id                        └───────┘        └─┘           └─┘ 
src                       └───────┘         └─┘             └─┘
typ                       └───────┘        └─┘           └─┘ 
168    s ∩ (⋂ i, t i) = ⋂ i, s ∩ t i :=
id                   
src                      
typ                  
doc                     
169  by rw [Inter_inter_distrib, Inter_const]
id          └─────────────────┘  └─────────┘
src     └──┘└─────────────────┘└┘└─────────┘└─
typ     └──┘└─────────────────┘└┘└─────────┘└─
doc     └──┘                   └┘           └─
txt     └──┘                   └┘           └─
par     └──┘                   └┘           └─
pid       └┘                   └┘           
st     └──────────────────────┘└───────────┘
170  
src  
typ  
doc  
txt  
par  
pid  
st   
171  theorem Inter_inter [inhabited ι] (s : set β) (t : ι → set β) :
id                        └───────┘        └─┘           └─┘ 
src                       └───────┘         └─┘             └─┘
typ                       └───────┘        └─┘           └─┘ 
172    (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
id                   
src                        
typ                  
doc                     
173  by rw [Inter_inter_distrib, Inter_const]
id          └─────────────────┘  └─────────┘
src     └──┘└─────────────────┘└┘└─────────┘└─
typ     └──┘└─────────────────┘└┘└─────────┘└─
doc     └──┘                   └┘           └─
txt     └──┘                   └┘           └─
par     └──┘                   └┘           └─
pid       └┘                   └┘           
st     └──────────────────────┘└───────────┘
174  
src  
typ  
doc  
txt  
par  
pid  
st   
175  -- classical
src  ────────────┘
typ  ────────────┘
doc  ────────────┘
txt  ────────────┘
par  ────────────┘
pid  ────────────┘
st   ────────────┘
176  theorem union_Inter (s : set β) (t : ι → set β) :
id                            └─┘           └─┘ 
src                           └─┘             └─┘
typ                           └─┘           └─┘ 
177    s ∪ (⋂ i, t i) = ⋂ i, s ∪ t i :=
id                   
src                      
typ                  
doc                     
178  ext $ assume x, by simp [classical.forall_or_distrib_left]
id   └─┘                     └──────────────────────────────┘
src  └─┘                └────┘└──────────────────────────────┘└─
typ  └─┘               └────┘└──────────────────────────────┘└─
doc                     └────┘                                └─
txt                     └────┘                                └─
par                     └────┘                                └─
pid                                                         
st                     └────────────────────────────────────────
179  
src  
typ  
doc  
txt  
par  
pid  
st   
180  theorem Union_diff (s : set β) (t : ι → set β) :
id                           └─┘           └─┘ 
src                          └─┘             └─┘
typ                          └─┘           └─┘ 
181    (⋃ i, t i) \ s = ⋃ i, t i \ s :=
id                   
src                        
typ                  
doc                     
182  Union_inter _ _
id   └─────────┘
src  └─────────┘
typ  └─────────┘
183  
184  theorem diff_Union [inhabited ι] (s : set β) (t : ι → set β) :
id                       └───────┘        └─┘           └─┘ 
src                      └───────┘         └─┘             └─┘
typ                      └───────┘        └─┘           └─┘ 
185    s \ (⋃ i, t i) = ⋂ i, s \ t i :=
id                   
src                      
typ                  
doc                     
186  by rw [diff_eq, compl_Union, inter_Inter]; refl
id          └─────┘  └─────────┘  └─────────┘
src     └──┘└─────┘└┘└─────────┘└┘└─────────┘  └────
typ     └──┘└─────┘└┘└─────────┘└┘└─────────┘  └────
doc     └──┘       └┘           └┘             └────
txt     └──┘       └┘           └┘             └────
par     └──┘       └┘           └┘             └────
pid       └┘       └┘           └┘                 
st     └──────────┘└───────────┘└───────────┘└──────
187  
src  
typ  
doc  
txt  
par  
pid  
st   
188  theorem diff_Inter (s : set β) (t : ι → set β) :
id                           └─┘           └─┘ 
src                          └─┘             └─┘
typ                          └─┘           └─┘ 
189    s \ (⋂ i, t i) = ⋃ i, s \ t i :=
id                   
src                      
typ                  
doc                     
190  by rw [diff_eq, compl_Inter, inter_Union]; refl
id          └─────┘  └─────────┘  └─────────┘
src     └──┘└─────┘└┘└─────────┘└┘└─────────┘  └────
typ     └──┘└─────┘└┘└─────────┘└┘└─────────┘  └────
doc     └──┘       └┘           └┘             └────
txt     └──┘       └┘           └┘             └────
par     └──┘       └┘           └┘             └────
pid       └┘       └┘           └┘                 
st     └──────────┘└───────────┘└───────────┘└──────
191  
src  
typ  
doc  
txt  
par  
pid  
st   
192  /- bounded unions and intersections -/
src  ───────────────────────────────────────
typ  ───────────────────────────────────────
doc  ───────────────────────────────────────
txt  ───────────────────────────────────────
par  ───────────────────────────────────────
pid  ───────────────────────────────────────
st   ───────────────────────────────────────
193  
src  
typ  
doc  
txt  
par  
pid  
st   
194  theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
id                               └─┘           └─┘        
src                              └─┘             └─┘
typ                              └─┘           └─┘        
195    y ∈ (⋃ x ∈ s, t x) ↔ ∃ x ∈ s, y ∈ t x := by simp
id                         
src                                         └────
typ                               └────
doc                                              └────
txt                                                └────
par                                                └────
pid                                                    
st                                                └─────
196  
src  
typ  
doc  
txt  
par  
pid  
st   
197  theorem mem_bInter_iff {s : set α} {t : α → set β} {y : β} :
id                               └─┘           └─┘        
src                              └─┘             └─┘
typ                              └─┘           └─┘        
198    y ∈ (⋂ x ∈ s, t x) ↔ ∀ x ∈ s, y ∈ t x := by simp
id                           
src                                           └────
typ                                 └────
doc                                              └────
txt                                                └────
par                                                └────
pid                                                    
st                                                └─────
199  
src  
typ  
doc  
txt  
par  
pid  
st   
200  theorem mem_bUnion {s : set α} {t : α → set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) :
id                           └─┘           └─┘                                     
src                          └─┘             └─┘                                         
typ                          └─┘           └─┘                                     
201    y ∈ ⋃ x ∈ s, t x :=
id             
src             
typ            
doc              
202  by simp; exact ⟨x, ⟨xs, ytx⟩⟩
id                      └┘  └─┘
src     └──┘  └────┘  └┘   └┘   └──
typ     └──┘  └────┘ └┘ └┘└┘└─┘└──
doc     └──┘  └────┘  └┘   └┘   └──
txt     └──┘  └────┘  └┘   └┘   └──
par     └──┘  └────┘  └┘   └┘   └──
pid                  └┘   └┘   └┘
st     └───────────────────────────
203  
src  
typ  
doc  
txt  
par  
pid  
st   
204  theorem mem_bInter {s : set α} {t : α → set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) :
id                           └─┘           └─┘                         
src                          └─┘             └─┘                            
typ                          └─┘           └─┘                         
205    y ∈ ⋂ x ∈ s, t x :=
id             
src             
typ            
doc              
206  by simp; assumption
src     └──┘  └──────────
typ     └──┘  └──────────
doc     └──┘  └──────────
txt     └──┘  └──────────
par     └──┘  └──────────
pid                     
st     └─────────────────
207  
src  
typ  
doc  
txt  
par  
pid  
st   
208  theorem bUnion_subset {s : set α} {t : set β} {u : α → set β} (h : ∀ x ∈ s, u x ⊆ t) :
id                              └─┘        └─┘           └─┘                  
src                             └─┘         └─┘             └─┘                      
typ                             └─┘        └─┘           └─┘                  
209    (⋃ x ∈ s, u x) ⊆ t :=
id               
src                 
typ              
doc           
210  show (⨆ x ∈ s, u x) ≤ t, -- TODO: should not be necessary when sets' order is based on lattices
id                  
src                    
typ                 
doc              
211    from supr_le $ assume x, supr_le (h x)
id          └─────┘            └─────┘   
src         └─────┘             └─────┘
typ         └─────┘            └─────┘   
212  
213  theorem subset_bInter {s : set α} {t : set β} {u : α → set β} (h : ∀ x ∈ s, t ⊆ u x) :
id                              └─┘        └─┘           └─┘                  
src                             └─┘         └─┘             └─┘                    
typ                             └─┘        └─┘           └─┘                  
214    t ⊆ (⋂ x ∈ s, u x) :=
id              
src              
typ             
doc               
215  subset_Inter $ assume x, subset_Inter $ h x
id   └──────────┘            └──────────┘    
src  └──────────┘             └──────────┘
typ  └──────────┘            └──────────┘    
216  
217  theorem subset_bUnion_of_mem {s : set α} {u : α → set β} {x : α} (xs : x ∈ s) :
id                                     └─┘           └─┘                  
src                                    └─┘             └─┘                    
typ                                    └─┘           └─┘                  
218    u x ⊆ (⋃ x ∈ s, u x) :=
id               
src                
typ              
doc                 
219  show u x ≤ (⨆ x ∈ s, u x),
id                  
src                   
typ                 
doc                    
220    from le_supr_of_le x $ le_supr _ xs
id          └───────────┘    └─────┘   └┘
src         └───────────┘     └─────┘
typ         └───────────┘    └─────┘   └┘
221  
222  theorem bInter_subset_of_mem {s : set α} {t : α → set β} {x : α} (xs : x ∈ s) :
id                                     └─┘           └─┘                  
src                                    └─┘             └─┘                    
typ                                    └─┘           └─┘                  
223    (⋂ x ∈ s, t x) ⊆ t x :=
id                
src                 
typ               
doc           
224  show (⨅x ∈ s, t x) ≤ t x,
id                  
src                   
typ                 
doc             
225    from infi_le_of_le x $ infi_le _ xs
id          └───────────┘    └─────┘   └┘
src         └───────────┘     └─────┘
typ         └───────────┘    └─────┘   └┘
226  
227  theorem bUnion_subset_bUnion_left {s s' : set α} {t : α → set β}
id                                             └─┘           └─┘ 
src                                            └─┘             └─┘
typ                                            └─┘           └─┘ 
228    (h : s ⊆ s') : (⋃ x ∈ s, t x) ⊆ (⋃ x ∈ s', t x) :=
id            └┘                   └┘  
src                                        
typ           └┘                   └┘  
doc                                          
229  bUnion_subset (λ x xs, subset_bUnion_of_mem (h xs))
id   └───────────┘     └┘  └──────────────────┘   └┘
src  └───────────┘          └──────────────────┘
typ  └───────────┘     └┘  └──────────────────┘   └┘
230  
231  theorem bInter_subset_bInter_left {s s' : set α} {t : α → set β}
id                                             └─┘           └─┘ 
src                                            └─┘             └─┘
typ                                            └─┘           └─┘ 
232    (h : s' ⊆ s) : (⋂ x ∈ s, t x) ⊆ (⋂ x ∈ s', t x) :=
id          └┘                     └┘  
src                                        
typ         └┘                     └┘  
doc                                          
233  subset_bInter (λ x xs, bInter_subset_of_mem (h xs))
id   └───────────┘     └┘  └──────────────────┘   └┘
src  └───────────┘          └──────────────────┘
typ  └───────────┘     └┘  └──────────────────┘   └┘
234  
235  theorem bUnion_subset_bUnion_right {s : set α} {t1 t2 : α → set β}
id                                           └─┘               └─┘ 
src                                          └─┘                 └─┘
typ                                          └─┘               └─┘ 
236    (h : ∀ x ∈ s, t1 x ⊆ t2 x) : (⋃ x ∈ s, t1 x) ⊆ (⋃ x ∈ s, t2 x) :=
id                 └┘   └┘           └┘          └┘ 
src                                                      
typ                └┘   └┘           └┘          └┘ 
doc                                                        
237  bUnion_subset (λ x xs, subset.trans (h x xs) (subset_bUnion_of_mem xs))
id   └───────────┘     └┘  └──────────┘    └┘   └──────────────────┘ └┘
src  └───────────┘          └──────────┘           └──────────────────┘
typ  └───────────┘     └┘  └──────────┘    └┘   └──────────────────┘ └┘
238  
239  theorem bInter_subset_bInter_right {s : set α} {t1 t2 : α → set β}
id                                           └─┘               └─┘ 
src                                          └─┘                 └─┘
typ                                          └─┘               └─┘ 
240    (h : ∀ x ∈ s, t1 x ⊆ t2 x) : (⋂ x ∈ s, t1 x) ⊆ (⋂ x ∈ s, t2 x) :=
id                 └┘   └┘           └┘          └┘ 
src                                                      
typ                └┘   └┘           └┘          └┘ 
doc                                                        
241  subset_bInter (λ x xs, subset.trans (bInter_subset_of_mem xs) (h x xs))
id   └───────────┘     └┘  └──────────┘  └──────────────────┘ └┘     └┘
src  └───────────┘          └──────────┘  └──────────────────┘
typ  └───────────┘     └┘  └──────────┘  └──────────────────┘ └┘     └┘
242  
243  theorem bUnion_eq_Union (s : set α) (t : α → set β) : (⋃ x ∈ s, t x) = (⋃ x : s, t x.1) :=
id                                └─┘           └─┘                       
src                               └─┘             └─┘                               
typ                               └─┘           └─┘                       
doc                                                                              
244  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
245  
src  
typ  
doc  
txt  
par  
pid  
st   
246  theorem bInter_eq_Inter (s : set α) (t : α → set β) : (⋂ x ∈ s, t x) = (⋂ x : s, t x.1) :=
id                                └─┘           └─┘                       
src                               └─┘             └─┘                               
typ                               └─┘           └─┘                       
doc                                                                              
247  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
248  
src  
typ  
doc  
txt  
par  
pid  
st   
249  @[simp] theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=
id                                        └─┘              └─┘       └──┘
src                                        └─┘                └─┘          └──┘
typ                                       └─┘              └─┘       └──┘
doc    └──┘                                                          
250  show (⨅x ∈ (∅ : set α), u x) = ⊤, -- simplifier should be able to rewrite x ∈ ∅ to false.
id                └─┘       
src                └─┘          
typ               └─┘       
doc                       
251    from infi_emptyset
id          └───────────┘
src         └───────────┘
typ         └───────────┘
252  
253  @[simp] theorem bInter_univ (u : α → set β) : (⋂ x ∈ @univ α, u x) = ⋂ x, u x :=
id                                       └─┘           └──┘         
src                                       └─┘             └──┘           
typ                                      └─┘           └──┘         
doc    └──┘                                                               
254  infi_univ
id   └───────┘
src  └───────┘
typ  └───────┘
255  
256  
257  -- TODO(Jeremy): here is an artifact of the the encoding of bounded intersection:
258  -- without dsimp, the next theorem fails to type check, because there is a lambda
259  -- in a type that needs to be contracted. Using simp [eq_of_mem_singleton xa] also works.
260  
261  @[simp] theorem bInter_singleton (a : α) (s : α → set β) : (⋂ x ∈ ({a} : set α), s x) = s a :=
id                                                   └─┘               └─┘        
src                                                    └─┘                  └─┘         
typ                                                  └─┘               └─┘        
doc    └──┘                                                                        
262  show (⨅ x ∈ ({a} : set α), s x) = s a, by simp
id                  └─┘        
src                   └─┘                  └────
typ                 └─┘             └────
doc                                          └────
txt                                            └────
par                                            └────
pid                                                
st                                            └─────
263  
src  
typ  
doc  
txt  
par  
pid  
st   
264  theorem bInter_union (s t : set α) (u : α → set β) :
id                               └─┘           └─┘ 
src                              └─┘             └─┘
typ                              └─┘           └─┘ 
265    (⋂ x ∈ s ∪ t, u x) = (⋂ x ∈ s, u x) ∩ (⋂ x ∈ t, u x) :=
id                                  
src                                          
typ                                 
doc                                             
266  show (⨅ x ∈ s ∪ t, u x) = (⨅ x ∈ s, u x) ⊓ (⨅ x ∈ t, u x),
id                                     
src                                             
typ                                    
doc                                                
267    from infi_union
id          └────────┘
src         └────────┘
typ         └────────┘
268  
269  -- TODO(Jeremy): simp [insert_eq, bInter_union] doesn't work
270  @[simp] theorem bInter_insert (a : α) (s : set α) (t : α → set β) :
id                                             └─┘           └─┘ 
src                                             └─┘             └─┘
typ                                            └─┘           └─┘ 
doc    └──┘
271    (⋂ x ∈ insert a s, t x) = t a ∩ (⋂ x ∈ s, t x) :=
id          └────┘                 
src          └────┘                       
typ         └────┘                 
doc                                         
272  begin rw insert_eq, simp [bInter_union] end
id            └───────┘        └──────────┘
src        └─┘└───────┘  └────┘└──────────┘└┘
typ        └─┘└───────┘  └────┘└──────────┘└┘
doc        └─┘           └────┘            └┘
txt        └─┘           └────┘            └┘
par        └─┘           └────┘            └┘
pid                                     
st   └────────────────┘└────────────────────┘└─┘
273  
274  -- TODO(Jeremy): another example of where an annotation is needed
275  
276  theorem bInter_pair (a b : α) (s : α → set β) :
id                                        └─┘ 
src                                         └─┘
typ                                       └─┘ 
277    (⋂ x ∈ ({a, b} : set α), s x) = s a ∩ s b :=
id                └─┘           
src                  └─┘              
typ               └─┘           
doc                          
278  by rw insert_of_has_insert; simp [inter_comm]
id         └──────────────────┘        └────────┘
src     └─┘└──────────────────┘  └────┘└────────┘└─
typ     └─┘└──────────────────┘  └────┘└────────┘└─
doc     └─┘                      └────┘          └─
txt     └─┘                      └────┘          └─
par     └─┘                      └────┘          └─
pid                                           
st     └───────────────────────────────────────────
279  
src  
typ  
doc  
txt  
par  
pid  
st   
280  @[simp] theorem bUnion_empty (s : α → set β) : (⋃ x ∈ (∅ : set α), s x) = ∅ :=
id                                        └─┘              └─┘       
src                                        └─┘                └─┘          
typ                                       └─┘              └─┘       
doc    └──┘                                                          
281  supr_emptyset
id   └───────────┘
src  └───────────┘
typ  └───────────┘
282  
283  @[simp] theorem bUnion_univ (s : α → set β) : (⋃ x ∈ @univ α, s x) = ⋃ x, s x :=
id                                       └─┘           └──┘         
src                                       └─┘             └──┘           
typ                                      └─┘           └──┘         
doc    └──┘                                                               
284  supr_univ
id   └───────┘
src  └───────┘
typ  └───────┘
285  
286  @[simp] theorem bUnion_singleton (a : α) (s : α → set β) : (⋃ x ∈ ({a} : set α), s x) = s a :=
id                                                   └─┘               └─┘        
src                                                    └─┘                  └─┘         
typ                                                  └─┘               └─┘        
doc    └──┘                                                                        
287  supr_singleton
id   └────────────┘
src  └────────────┘
typ  └────────────┘
288  
289  @[simp] theorem bUnion_of_singleton (s : set α) : (⋃ x ∈ s, {x}) = s :=
id                                            └─┘               
src                                           └─┘                  
typ                                           └─┘               
doc    └──┘                                                   
290  ext $ by simp
id   └─┘
src  └─┘      └────
typ  └─┘      └────
doc           └────
txt           └────
par           └────
pid               
st           └─────
291  
src  
typ  
doc  
txt  
par  
pid  
st   
292  theorem bUnion_union (s t : set α) (u : α → set β) :
id                               └─┘           └─┘ 
src                              └─┘             └─┘
typ                              └─┘           └─┘ 
293    (⋃ x ∈ s ∪ t, u x) = (⋃ x ∈ s, u x) ∪ (⋃ x ∈ t, u x) :=
id                                  
src                                          
typ                                 
doc                                             
294  supr_union
id   └────────┘
src  └────────┘
typ  └────────┘
295  
296  -- TODO(Jeremy): once again, simp doesn't do it alone.
297  
298  @[simp] theorem bUnion_insert (a : α) (s : set α) (t : α → set β) :
id                                             └─┘           └─┘ 
src                                             └─┘             └─┘
typ                                            └─┘           └─┘ 
doc    └──┘
299    (⋃ x ∈ insert a s, t x) = t a ∪ (⋃ x ∈ s, t x) :=
id          └────┘                 
src          └────┘                       
typ         └────┘                 
doc                                         
300  begin rw [insert_eq], simp [bUnion_union] end
id             └───────┘         └──────────┘
src        └──┘└───────┘  └────┘└──────────┘└┘
typ        └──┘└───────┘  └────┘└──────────┘└┘
doc        └──┘           └────┘            └┘
txt        └──┘           └────┘            └┘
par        └──┘           └────┘            └┘
pid          └┘                           
st   └─────────────────┘└─────────────────────┘└─┘
301  
302  theorem bUnion_pair (a b : α) (s : α → set β) :
id                                        └─┘ 
src                                         └─┘
typ                                       └─┘ 
303    (⋃ x ∈ ({a, b} : set α), s x) = s a ∪ s b :=
id                └─┘           
src                  └─┘              
typ               └─┘           
doc                          
304  by rw insert_of_has_insert; simp [union_comm]
id         └──────────────────┘        └────────┘
src     └─┘└──────────────────┘  └────┘└────────┘└─
typ     └─┘└──────────────────┘  └────┘└────────┘└─
doc     └─┘                      └────┘          └─
txt     └─┘                      └────┘          └─
par     └─┘                      └────┘          └─
pid                                           
st     └───────────────────────────────────────────
305  
src  
typ  
doc  
txt  
par  
pid  
st   
306  @[simp] -- complete_boolean_algebra
doc    └──┘
307  theorem compl_bUnion (s : set α) (t : α → set β) : - (⋃ i ∈ s, t i) = (⋂ i ∈ s, - t i) :=
id                             └─┘           └─┘                        
src                            └─┘             └─┘                             
typ                            └─┘           └─┘                        
doc                                                                             
308  ext (λ x, by simp)
id   └─┘    
src  └─┘          └──┘
typ  └─┘         └──┘
doc               └──┘
txt               └──┘
par               └──┘
st               └───┘
309  
310  -- classical -- complete_boolean_algebra
311  theorem compl_bInter (s : set α) (t : α → set β) : -(⋂ i ∈ s, t i) = (⋃ i ∈ s, - t i) :=
id                             └─┘           └─┘                       
src                            └─┘             └─┘                            
typ                            └─┘           └─┘                       
doc                                                                            
312  ext (λ x, by simp [classical.not_forall])
id   └─┘               └──────────────────┘
src  └─┘          └────┘└──────────────────┘
typ  └─┘         └────┘└──────────────────┘
doc               └────┘                    
txt               └────┘                    
par               └────┘                    
pid                                       
st               └──────────────────────────┘
313  
314  theorem inter_bUnion (s : set α) (t : α → set β) (u : set β) :
id                             └─┘           └─┘        └─┘ 
src                            └─┘             └─┘         └─┘
typ                            └─┘           └─┘        └─┘ 
315    u ∩ (⋃ i ∈ s, t i) = ⋃ i ∈ s, u ∩ t i :=
id                         
src                              
typ                        
doc                             
316  begin
st   └─────
317    ext x,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
318    simp only [exists_prop, mem_Union, mem_inter_eq],
id                └─────────┘  └───────┘  └──────────┘
src    └─────────┘└─────────┘└┘└───────┘└┘└──────────┘
typ    └─────────┘└─────────┘└┘└───────┘└┘└──────────┘
doc    └─────────┘           └┘         └┘            
txt    └─────────┘           └┘         └┘            
par    └─────────┘           └┘         └┘            
pid        └──┘└┘           └┘         └┘            
st   ─────────────────────────────────────────────────┘└─
319    exact ⟨λ ⟨hx, ⟨i, is, xi⟩⟩, ⟨i, is, hx, xi⟩, λ ⟨i, is, hx, xi⟩, ⟨hx, ⟨i, is, xi⟩⟩⟩
id               └┘     └┘  └┘                          └┘  └┘  └┘
src    └────┘  └┘  └┘  └┘  └┘  └──┘  └┘  └┘  └┘  └─┘ └┘ └┘  └┘  └┘  └─┘   └┘  └┘  └┘  └──┘
typ    └────┘  └┘└┘└┘ └┘└┘└┘└┘└──┘  └┘  └┘  └┘  └─┘ └┘└┘└┘└┘└┘└┘└┘└─┘   └┘  └┘  └┘  └──┘
doc    └────┘  └┘  └┘  └┘  └┘  └──┘  └┘  └┘  └┘  └─┘ └┘ └┘  └┘  └┘  └─┘   └┘  └┘  └┘  └──┘
txt    └────┘  └┘  └┘  └┘  └┘  └──┘  └┘  └┘  └┘  └─┘ └┘ └┘  └┘  └┘  └─┘   └┘  └┘  └┘  └──┘
par    └────┘  └┘  └┘  └┘  └┘  └──┘  └┘  └┘  └┘  └─┘ └┘ └┘  └┘  └┘  └─┘   └┘  └┘  └┘  └──┘
pid           └┘  └┘  └┘  └┘  └──┘  └┘  └┘  └┘  └─┘ └┘ └┘  └┘  └┘  └─┘   └┘  └┘  └┘  └─┘
st   ────────────────────────────────────────────────────────────────────────────────────┘
320  end
st   └─┘
321  
322  theorem bUnion_inter (s : set α) (t : α → set β) (u : set β) :
id                             └─┘           └─┘        └─┘ 
src                            └─┘             └─┘         └─┘
typ                            └─┘           └─┘        └─┘ 
323    (⋃ i ∈ s, t i) ∩ u = (⋃ i ∈ s, t i ∩ u) :=
id                          
src                                 
typ                         
doc                              
324  by simp [@inter_comm _ _ u, inter_bUnion]
id             └────────┘       └──────────┘
src     └────┘ └────────┘└───┘ └┘└──────────┘└─
typ     └────┘ └────────┘└───┘└┘└──────────┘└─
doc     └────┘           └───┘ └┘            └─
txt     └────┘           └───┘ └┘            └─
par     └────┘           └───┘ └┘            └─
pid                    └───┘ └┘            
st     └───────────────────────────────────────
325  
src  
typ  
doc  
txt  
par  
pid  
st   
326  /-- Intersection of a set of sets. -/
327  @[reducible] def sInter (S : set (set α)) : set α := Inf S
id                                └─┘  └─┘      └─┘     └─┘ 
src                               └─┘  └─┘       └─┘      └─┘
typ                               └─┘  └─┘      └─┘     └─┘ 
doc    └───────┘                                          └─┘
328  
329  prefix `⋂₀`:110 := sInter
id                      └────┘
src                     └────┘
typ                     └────┘
doc                     └────┘
330  
331  theorem mem_sUnion_of_mem {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :
id                                         └─┘        └─┘  └─┘                      
src                                         └─┘         └─┘  └─┘                         
typ                                        └─┘        └─┘  └─┘                      
332    x ∈ ⋃₀ S :=
id       └┘ 
src       └┘
typ      └┘ 
333  ⟨t, ⟨ht, hx⟩⟩
id       └┘  └┘
typ      └┘  └┘
334  
335  @[simp] theorem mem_sUnion {x : α} {S : set (set α)} : x ∈ ⋃₀ S ↔ ∃t ∈ S, x ∈ t := iff.rfl
id                                          └─┘  └─┘        └┘             └─────┘
src                                          └─┘  └─┘          └┘                  └─────┘
typ                                         └─┘  └─┘        └┘             └─────┘
doc    └──┘
336  
337  -- is this theorem really necessary?
338  theorem not_mem_of_not_mem_sUnion {x : α} {t : set α} {S : set (set α)}
id                                                 └─┘        └─┘  └─┘ 
src                                                 └─┘         └─┘  └─┘
typ                                                └─┘        └─┘  └─┘ 
339    (hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t :=
id             └┘                 
src             └┘                    
typ            └┘                 
340  λ h, hx ⟨t, ht, h⟩
id       └┘    └┘  
typ      └┘    └┘  
341  
342  @[simp] theorem mem_sInter {x : α} {S : set (set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t := iff.rfl
id                                          └─┘  └─┘        └┘                └─────┘
src                                          └─┘  └─┘          └┘                     └─────┘
typ                                         └─┘  └─┘        └┘                └─────┘
doc    └──┘                                                     └┘
343  
344  theorem sInter_subset_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : ⋂₀ S ⊆ t :=
id                                     └─┘  └─┘         └─┘               └┘   
src                                    └─┘  └─┘          └─┘                  └┘   
typ                                    └─┘  └─┘         └─┘               └┘   
doc                                                                            └┘
345  Inf_le tS
id   └────┘ └┘
src  └────┘
typ  └────┘ └┘
346  
347  theorem subset_sUnion_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : t ⊆ ⋃₀ S :=
id                                     └─┘  └─┘         └─┘                 └┘ 
src                                    └─┘  └─┘          └─┘                     └┘
typ                                    └─┘  └─┘         └─┘                 └┘ 
348  le_Sup tS
id   └────┘ └┘
src  └────┘
typ  └────┘ └┘
349  
350  lemma subset_sUnion_of_subset {s : set α} (t : set (set α)) (u : set α) (h₁ : s ⊆ u)
id                                      └─┘        └─┘  └─┘         └─┘           
src                                     └─┘         └─┘  └─┘          └─┘            
typ                                     └─┘        └─┘  └─┘         └─┘           
351    (h₂ : u ∈ t) : s ⊆ ⋃₀ t :=
id                   └┘ 
src                     └┘
typ                  └┘ 
352  subset.trans h₁ (subset_sUnion_of_mem h₂)
id   └──────────┘ └┘  └──────────────────┘ └┘
src  └──────────┘     └──────────────────┘
typ  └──────────┘ └┘  └──────────────────┘ └┘
353  
354  theorem sUnion_subset {S : set (set α)} {t : set α} (h : ∀t' ∈ S, t' ⊆ t) : (⋃₀ S) ⊆ t :=
id                              └─┘  └─┘         └─┘         └┘     └┘       └┘    
src                             └─┘  └─┘          └─┘                            └┘    
typ                             └─┘  └─┘         └─┘         └┘     └┘       └┘    
355  Sup_le h
id   └────┘ 
src  └────┘
typ  └────┘ 
356  
357  theorem sUnion_subset_iff {s : set (set α)} {t : set α} : ⋃₀ s ⊆ t ↔ ∀t' ∈ s, t' ⊆ t :=
id                                  └─┘  └─┘         └─┘     └┘      └┘     └┘  
src                                 └─┘  └─┘          └─┘      └┘                   
typ                                 └─┘  └─┘         └─┘     └┘      └┘     └┘  
358  ⟨assume h t' ht', subset.trans (subset_sUnion_of_mem ht') h, sUnion_subset⟩
id            └┘ └─┘  └──────────┘  └──────────────────┘ └─┘    └───────────┘
src                    └──────────┘  └──────────────────┘         └───────────┘
typ           └┘ └─┘  └──────────┘  └──────────────────┘ └─┘    └───────────┘
359  
360  theorem subset_sInter {S : set (set α)} {t : set α} (h : ∀t' ∈ S, t ⊆ t') : t ⊆ (⋂₀ S) :=
id                              └─┘  └─┘         └─┘         └┘       └┘       └┘ 
src                             └─┘  └─┘          └─┘                               └┘
typ                             └─┘  └─┘         └─┘         └┘       └┘       └┘ 
doc                                                                                   └┘
361  le_Inf h
id   └────┘ 
src  └────┘
typ  └────┘ 
362  
363  theorem sUnion_subset_sUnion {S T : set (set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T :=
id                                       └─┘  └─┘               └┘   └┘ 
src                                      └─┘  └─┘                  └┘    └┘
typ                                      └─┘  └─┘               └┘   └┘ 
364  sUnion_subset $ λ s hs, subset_sUnion_of_mem (h hs)
id   └───────────┘      └┘  └──────────────────┘   └┘
src  └───────────┘           └──────────────────┘
typ  └───────────┘      └┘  └──────────────────┘   └┘
365  
366  theorem sInter_subset_sInter {S T : set (set α)} (h : S ⊆ T) : ⋂₀ T ⊆ ⋂₀ S :=
id                                       └─┘  └─┘               └┘   └┘ 
src                                      └─┘  └─┘                  └┘    └┘
typ                                      └─┘  └─┘               └┘   └┘ 
doc                                                                 └┘     └┘
367  subset_sInter $ λ s hs, sInter_subset_of_mem (h hs)
id   └───────────┘      └┘  └──────────────────┘   └┘
src  └───────────┘           └──────────────────┘
typ  └───────────┘      └┘  └──────────────────┘   └┘
368  
369  @[simp] theorem sUnion_empty : ⋃₀ ∅ = (∅ : set α) := Sup_empty
id                                  └┘       └─┘      └───────┘
src                                 └┘       └─┘       └───────┘
typ                                 └┘       └─┘      └───────┘
doc    └──┘
370  
371  @[simp] theorem sInter_empty : ⋂₀ ∅ = (univ : set α) := Inf_empty
id                                  └┘    └──┘   └─┘      └───────┘
src                                 └┘    └──┘   └─┘       └───────┘
typ                                 └┘    └──┘   └─┘      └───────┘
doc    └──┘                         └┘
372  
373  @[simp] theorem sUnion_singleton (s : set α) : ⋃₀ {s} = s := Sup_singleton
id                                         └─┘     └┘        └───────────┘
src                                        └─┘      └┘          └───────────┘
typ                                        └─┘     └┘        └───────────┘
doc    └──┘
374  
375  @[simp] theorem sInter_singleton (s : set α) : ⋂₀ {s} = s := Inf_singleton
id                                         └─┘     └┘        └───────────┘
src                                        └─┘      └┘          └───────────┘
typ                                        └─┘     └┘        └───────────┘
doc    └──┘                                         └┘
376  
377  theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T := Sup_union
id                               └─┘  └─┘      └┘       └┘   └┘     └───────┘
src                              └─┘  └─┘       └┘         └┘    └┘      └───────┘
typ                              └─┘  └─┘      └┘       └┘   └┘     └───────┘
378  
379  theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union
id                               └─┘  └─┘      └┘       └┘   └┘     └───────┘
src                              └─┘  └─┘       └┘         └┘    └┘      └───────┘
typ                              └─┘  └─┘      └┘       └┘   └┘     └───────┘
doc                                             └┘           └┘     └┘
380  
381  @[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T := Sup_insert
id                                      └─┘        └─┘  └─┘      └┘  └────┘       └┘     └────────┘
src                                     └─┘         └─┘  └─┘       └┘  └────┘          └┘      └────────┘
typ                                     └─┘        └─┘  └─┘      └┘  └────┘       └┘     └────────┘
doc    └──┘
382  
383  @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert
id                                      └─┘        └─┘  └─┘      └┘  └────┘       └┘     └────────┘
src                                     └─┘         └─┘  └─┘       └┘  └────┘          └┘      └────────┘
typ                                     └─┘        └─┘  └─┘      └┘  └────┘       └┘     └────────┘
doc    └──┘                                                        └┘                    └┘
384  
385  theorem sUnion_pair (s t : set α) : ⋃₀ {s, t} = s ∪ t :=
id                              └─┘     └┘       
src                             └─┘      └┘         
typ                             └─┘     └┘       
386  (sUnion_insert _ _).trans $ by rw [union_comm, sUnion_singleton]
id    └───────────┘     └───┘           └────────┘  └──────────────┘
src   └───────────┘     └───┘       └──┘└────────┘└┘└──────────────┘└─
typ   └───────────┘     └───┘       └──┘└────────┘└┘└──────────────┘└─
doc                                 └──┘          └┘                └─
txt                                 └──┘          └┘                └─
par                                 └──┘          └┘                └─
pid                                   └┘          └┘                
st                                 └─────────────┘└────────────────┘
387  
src  
typ  
doc  
txt  
par  
pid  
st   
388  theorem sInter_pair (s t : set α) : ⋂₀ {s, t} = s ∩ t :=
id                              └─┘     └┘       
src                             └─┘      └┘         
typ                             └─┘     └┘       
doc                                      └┘
389  (sInter_insert _ _).trans $ by rw [inter_comm, sInter_singleton]
id    └───────────┘     └───┘           └────────┘  └──────────────┘
src   └───────────┘     └───┘       └──┘└────────┘└┘└──────────────┘└─
typ   └───────────┘     └───┘       └──┘└────────┘└┘└──────────────┘└─
doc                                 └──┘          └┘                └─
txt                                 └──┘          └┘                └─
par                                 └──┘          └┘                └─
pid                                   └┘          └┘                
st                                 └─────────────┘└────────────────┘
390  
src  
typ  
doc  
txt  
par  
pid  
st   
391  @[simp] theorem sUnion_image (f : α → set β) (s : set α) : ⋃₀ (f '' s) = ⋃ x ∈ s, f x := Sup_image
id                                        └─┘        └─┘     └┘   └┘              └───────┘
src                                        └─┘         └─┘      └┘    └┘                   └───────┘
typ                                       └─┘        └─┘     └┘   └┘              └───────┘
doc    └──┘                                                                         
392  
393  @[simp] theorem sInter_image (f : α → set β) (s : set α) : ⋂₀ (f '' s) = ⋂ x ∈ s, f x := Inf_image
id                                        └─┘        └─┘     └┘   └┘              └───────┘
src                                        └─┘         └─┘      └┘    └┘                   └───────┘
typ                                       └─┘        └─┘     └┘   └┘              └───────┘
doc    └──┘                                                     └┘                  
394  
395  @[simp] theorem sUnion_range (f : ι → set β) : ⋃₀ (range f) = ⋃ x, f x := Sup_range
id                                        └─┘     └┘  └───┘           └───────┘
src                                        └─┘      └┘  └───┘               └───────┘
typ                                       └─┘     └┘  └───┘           └───────┘
doc    └──┘                                             └───┘        
396  
397  @[simp] theorem sInter_range (f : ι → set β) : ⋂₀ (range f) = ⋂ x, f x := Inf_range
id                                        └─┘     └┘  └───┘           └───────┘
src                                        └─┘      └┘  └───┘               └───────┘
typ                                       └─┘     └┘  └───┘           └───────┘
doc    └──┘                                         └┘  └───┘        
398  
399  lemma sUnion_eq_univ_iff {c : set (set α)} :
id                                 └─┘  └─┘ 
src                                └─┘  └─┘
typ                                └─┘  └─┘ 
400    ⋃₀ c = @set.univ α ↔ ∀ a, ∃ b ∈ c, a ∈ b :=
id     └┘    └──────┘              
src    └┘     └──────┘                  
typ    └┘    └──────┘              
401  ⟨λ H a, let ⟨b, hm, hb⟩ := mem_sUnion.1 $ by rw H; exact mem_univ a in ⟨b, hm, hb⟩,
id         └─┘    └┘  └┘     └────────┘                  └──────┘ 
src                             └────────┘       └─┘   └────┘└──────┘ 
typ        └─┘    └┘  └┘     └────────┘       └─┘  └────┘└──────┘
doc                                               └─┘   └────┘         
txt                                               └─┘   └────┘         
par                                               └─┘   └────┘         
pid                                                                  
st                                               └──────────────────────┘
402   λ H, set.univ_subset_iff.1 $ λ x hx, let ⟨b, hm, hb⟩ := H x in set.mem_sUnion_of_mem hb hm⟩
id        └─────────────────┘       └┘  └─┘     └┘  └┘          └───────────────────┘
src        └─────────────────┘                                      └───────────────────┘
typ       └─────────────────┘       └┘  └─┘     └┘  └┘          └───────────────────┘
403  
404  theorem compl_sUnion (S : set (set α)) :
id                             └─┘  └─┘ 
src                            └─┘  └─┘
typ                            └─┘  └─┘ 
405    - ⋃₀ S = ⋂₀ (compl '' S) :=
id      └┘   └┘  └───┘ └┘ 
src     └┘    └┘  └───┘ └┘
typ     └┘   └┘  └───┘ └┘ 
doc             └┘
406  set.ext $ assume x,
id   └─────┘          
src  └─────┘
typ  └─────┘          
407    ⟨assume : ¬ (∃s∈S, x ∈ s), assume s h,
id                                
src                      
typ                               
408      match s, h with
id               
typ              
409      ._, ⟨t, hs, rfl⟩ := assume h, this ⟨t, hs, h⟩
id              └┘  └─┘              └──┘         
src                  └─┘
typ             └┘  └─┘              └──┘         
410      end,
411      assume : ∀s, s ∈ compl '' S → x ∈ s,
id                     └───┘ └┘      
src                      └───┘ └┘       
typ                    └───┘ └┘      
412      assume ⟨t, tS, xt⟩, this (compl t) (mem_image_of_mem _ tS) xt⟩
id                └┘  └┘   └──┘  └───┘     └──────────────┘
src                                └───┘     └──────────────┘
typ               └┘  └┘   └──┘  └───┘     └──────────────┘
413  
414  -- classical
415  theorem sUnion_eq_compl_sInter_compl (S : set (set α)) :
id                                             └─┘  └─┘ 
src                                            └─┘  └─┘
typ                                            └─┘  └─┘ 
416    ⋃₀ S = - ⋂₀ (compl '' S) :=
id     └┘    └┘  └───┘ └┘ 
src    └┘     └┘  └───┘ └┘
typ    └┘    └┘  └───┘ └┘ 
doc             └┘
417  by rw [←compl_compl (⋃₀ S), compl_sUnion]
id           └─────────┘  └┘    └──────────┘
src     └───┘└─────────┘ └┘ └─┘└──────────┘└─
typ     └───┘└─────────┘ └┘└─┘└──────────┘└─
doc     └───┘               └─┘            └─
txt     └───┘               └─┘            └─
par     └───┘               └─┘            └─
pid       └─┘               └─┘            
st     └──────────────────────┘└────────────┘
418  
src  
typ  
doc  
txt  
par  
pid  
st   
419  -- classical
src  ────────────┘
typ  ────────────┘
doc  ────────────┘
txt  ────────────┘
par  ────────────┘
pid  ────────────┘
st   ────────────┘
420  theorem compl_sInter (S : set (set α)) :
id                             └─┘  └─┘ 
src                            └─┘  └─┘
typ                            └─┘  └─┘ 
421    - ⋂₀ S = ⋃₀ (compl '' S) :=
id      └┘   └┘  └───┘ └┘ 
src     └┘    └┘  └───┘ └┘
typ     └┘   └┘  └───┘ └┘ 
doc      └┘
422  by rw [sUnion_eq_compl_sInter_compl, compl_compl_image]
id          └──────────────────────────┘  └───────────────┘
src     └──┘└──────────────────────────┘└┘└───────────────┘└─
typ     └──┘└──────────────────────────┘└┘└───────────────┘└─
doc     └──┘                            └┘                 └─
txt     └──┘                            └┘                 └─
par     └──┘                            └┘                 └─
pid       └┘                            └┘                 
st     └───────────────────────────────┘└─────────────────┘
423  
src  
typ  
doc  
txt  
par  
pid  
st   
424  -- classical
src  ────────────┘
typ  ────────────┘
doc  ────────────┘
txt  ────────────┘
par  ────────────┘
pid  ────────────┘
st   ────────────┘
425  theorem sInter_eq_comp_sUnion_compl (S : set (set α)) :
id                                            └─┘  └─┘ 
src                                           └─┘  └─┘
typ                                           └─┘  └─┘ 
426     ⋂₀ S = -(⋃₀ (compl '' S)) :=
id      └┘    └┘  └───┘ └┘ 
src     └┘     └┘  └───┘ └┘
typ     └┘    └┘  └───┘ └┘ 
doc     └┘
427  by rw [←compl_compl (⋂₀ S), compl_sInter]
id           └─────────┘  └┘    └──────────┘
src     └───┘└─────────┘ └┘ └─┘└──────────┘└─
typ     └───┘└─────────┘ └┘└─┘└──────────┘└─
doc     └───┘            └┘ └─┘            └─
txt     └───┘               └─┘            └─
par     └───┘               └─┘            └─
pid       └─┘               └─┘            
st     └──────────────────────┘└────────────┘
428  
src  
typ  
doc  
txt  
par  
pid  
st   
429  theorem inter_empty_of_inter_sUnion_empty {s t : set α} {S : set (set α)} (hs : t ∈ S)
id                                                    └─┘        └─┘  └─┘            
src                                                   └─┘         └─┘  └─┘             
typ                                                   └─┘        └─┘  └─┘            
430      (h : s ∩ ⋃₀ S = ∅) :
id              └┘   
src              └┘    
typ             └┘   
431    s ∩ t = ∅ :=
id         
src          
typ        
432  eq_empty_of_subset_empty $ by rw ← h; exact
id   └──────────────────────┘           
src  └──────────────────────┘      └───┘   └────┘
typ  └──────────────────────┘      └───┘  └────┘
doc                                └───┘   └────┘
txt                                └───┘   └────┘
par                                └───┘   └────┘
pid                                  └─┘        
st                                └──────────────
433  inter_subset_inter_right _ (subset_sUnion_of_mem hs)
id   └──────────────────────┘    └──────────────────┘ └┘
src  └──────────────────────┘└─┘ └──────────────────┘  └─
typ  └──────────────────────┘└─┘ └──────────────────┘└┘└─
doc                          └─┘                       └─
txt                          └─┘                       └─
par                          └─┘                       └─
pid                          └─┘                       
st   ─────────────────────────────────────────────────────
434  
src  
typ  
doc  
txt  
par  
pid  
st   
435  theorem range_sigma_eq_Union_range {γ : α → Type*} (f : sigma γ → β) :
id                                                          └───┘    
src                                                          └───┘
typ                                                         └───┘    
436    range f = ⋃ a, range (λ b, f ⟨a, b⟩) :=
id     └───┘     └───┘          
src    └───┘       └───┘
typ    └───┘     └───┘          
doc    └───┘        └───┘
437  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
438  
src  
typ  
doc  
txt  
par  
pid  
st   
439  theorem Union_eq_range_sigma (s : α → set β) : (⋃ i, s i) = range (λ a : Σ i, s i, a.2) :=
id                                        └─┘            └───┘             
src                                        └─┘                └───┘                 
typ                                       └─┘            └───┘             
doc                                                            └───┘
440  by simp [set.ext_iff]
id            └─────────┘
src     └────┘└─────────┘└─
typ     └────┘└─────────┘└─
doc     └────┘           └─
txt     └────┘           └─
par     └────┘           └─
pid                    
st     └───────────────────
441  
src  
typ  
doc  
txt  
par  
pid  
st   
442  theorem Union_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : set (sigma σ)) :
id                                                                                 └─┘  └───┘ 
src                                                                                 └─┘  └───┘
typ                                                                                └─┘  └───┘ 
443    (⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s)) = s :=
id        └──────┘  └┘  └──────┘  └─┘     
src        └──────┘   └┘  └──────┘   └─┘     
typ       └──────┘  └┘  └──────┘  └─┘     
doc                                  └─┘
444  begin
st   └─────
445    ext x,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
446    simp only [mem_Union, mem_image, mem_preimage],
id                └───────┘  └───────┘  └──────────┘
src    └─────────┘└───────┘└┘└───────┘└┘└──────────┘
typ    └─────────┘└───────┘└┘└───────┘└┘└──────────┘
doc    └─────────┘         └┘         └┘            
txt    └─────────┘         └┘         └┘            
par    └─────────┘         └┘         └┘            
pid        └──┘└┘         └┘         └┘            
st   ───────────────────────────────────────────────┘└─
447    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
448    { rintros ⟨i, a, h, rfl⟩, exact h },
id                                     
src      └────────────────────┘  └────┘ 
typ      └────────────────────┘  └────┘
doc      └────────────────────┘  └────┘ 
txt      └────────────────────┘  └────┘ 
par      └────────────────────┘  └────┘ 
pid             └─────────────┘        
st   ───┘└────────────────────┘└────────┘└┘
449    { intro h, cases x with i a, exact ⟨i, a, h, rfl⟩ }
id                                              └─┘
src      └─────┘  └────┘ └───────┘  └────┘  └┘ └┘ └┘└─┘└┘
typ      └─────┘  └────┘└───────┘  └────┘ └┘└┘└┘└─┘└┘
doc      └─────┘  └────┘ └───────┘  └────┘  └┘ └┘ └┘   └┘
txt      └─────┘  └────┘ └───────┘  └────┘  └┘ └┘ └┘   └┘
par      └─────┘  └────┘ └───────┘  └────┘  └┘ └┘ └┘   └┘
pid           └┘        └───────┘         └┘ └┘ └┘   
st   ──────────┘└────────────────┘└─────────────────────┘└─
450  end
st   ──┘
451  
452  lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) :=
id                            └─┘  └─┘                └┘     └┘ 
src                           └─┘  └─┘                   └┘      └┘
typ                           └─┘  └─┘                └┘     └┘ 
453  sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht'
id   └───────────┘          └┘ └─┘  └──────────────────┘    └─┘
src  └───────────┘                  └──────────────────┘
typ  └───────────┘          └┘ └─┘  └──────────────────┘    └─┘
454  
455  lemma Union_subset_Union {s t : ι → set α} (h : ∀i, s i ⊆ t i) : (⋃i, s i) ⊆ (⋃i, t i) :=
id                                      └─┘                            
src                                      └─┘                                    
typ                                     └─┘                            
doc                                                                               
456  @supr_le_supr (set α) ι _ s t h
id    └──────────┘  └─┘        
src   └──────────┘  └─┘
typ   └──────────┘  └─┘        
457  
458  lemma Union_subset_Union2 {ι₂ : Sort*} {s : ι → set α} {t : ι₂ → set α} (h : ∀i, ∃j, s i ⊆ t j) :
id                                                  └─┘        └┘   └─┘                
src                                                  └─┘              └─┘                   
typ                                                 └─┘        └┘   └─┘                
459    (⋃i, s i) ⊆ (⋃i, t i) :=
id              
src               
typ             
doc                
460  @supr_le_supr2 (set α) ι ι₂ _ s t h
id    └───────────┘  └─┘    └┘     
src   └───────────┘  └─┘
typ   └───────────┘  └─┘    └┘     
461  
462  lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) :=
id                                                     └─┘           └┘                └┘ 
src                                                    └─┘                                   
typ                                                    └─┘           └┘                └┘ 
doc                                                                                           
463  @supr_le_supr_const (set α) ι ι₂ _ s h
id    └────────────────┘  └─┘    └┘    
src   └────────────────┘  └─┘
typ   └────────────────┘  └─┘    └┘    
464  
465  @[simp] lemma Union_of_singleton (α : Type u) : (⋃(x : α), {x}) = @set.univ α :=
id                                                                └──────┘ 
src                                                                 └──────┘
typ                                                               └──────┘ 
doc    └──┘                                                  
466  ext $ λ x, ⟨λ h, ⟨⟩, λ h, ⟨{x}, ⟨⟨x, rfl⟩, mem_singleton x⟩⟩⟩
id   └─┘                           └─┘   └───────────┘ 
src  └─┘                                └─┘   └───────────┘
typ  └─┘                           └─┘   └───────────┘ 
467  
468  theorem bUnion_subset_Union (s : set α) (t : α → set β) :
id                                    └─┘           └─┘ 
src                                   └─┘             └─┘
typ                                   └─┘           └─┘ 
469    (⋃ x ∈ s, t x) ⊆ (⋃ x, t x) :=
id                   
src                     
typ                  
doc                      
470  Union_subset_Union $ λ i, Union_subset $ λ h, by refl
id   └────────────────┘       └──────────┘     
src  └────────────────┘        └──────────┘           └────
typ  └────────────────┘       └──────────┘          └────
doc                                                   └────
txt                                                   └────
par                                                   └────
pid                                                       
st                                                   └─────
471  
src  
typ  
doc  
txt  
par  
pid  
st   
472  lemma sUnion_eq_bUnion {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=
id                               └─┘  └─┘       └┘           └─┘            
src                              └─┘  └─┘        └┘            └─┘              
typ                              └─┘  └─┘       └┘           └─┘            
doc                                                                               
473  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
474  
src  
typ  
doc  
txt  
par  
pid  
st   
475  lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h : i ∈ s), i) :=
id                               └─┘  └─┘       └┘           └─┘            
src                              └─┘  └─┘        └┘            └─┘              
typ                              └─┘  └─┘       └┘           └─┘            
doc                                              └┘                               
476  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
477  
src  
typ  
doc  
txt  
par  
pid  
st   
478  lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i.1) :=
id                              └─┘  └─┘       └┘             
src                             └─┘  └─┘        └┘                
typ                             └─┘  └─┘       └┘             
doc                                                              
479  set.ext $ λ x, by simp
id   └─────┘     
src  └─────┘           └────
typ  └─────┘          └────
doc                    └────
txt                    └────
par                    └────
pid                        
st                    └─────
480  
src  
typ  
doc  
txt  
par  
pid  
st   
481  lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i.1) :=
id                              └─┘  └─┘       └┘             
src                             └─┘  └─┘        └┘                
typ                             └─┘  └─┘       └┘             
doc                                             └┘               
482  set.ext $ λ x, by simp
id   └─────┘     
src  └─────┘           └────
typ  └─────┘          └────
doc                    └────
txt                    └────
par                    └────
pid                        
st                    └─────
483  
src  
typ  
doc  
txt  
par  
pid  
st   
484  lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
id                                 └─┘     └┘  └┘       └──┘ └──┘  └┘ └┘
src                                └─┘                   └──┘ └──┘
typ                                └─┘     └┘  └┘       └──┘ └──┘  └┘ └┘
doc                                                            
485  set.ext $ λ x, by simp [bool.exists_bool, or_comm]
id   └─────┘                └──────────────┘  └─────┘
src  └─────┘           └────┘└──────────────┘└┘└─────┘└─
typ  └─────┘          └────┘└──────────────┘└┘└─────┘└─
doc                    └────┘                └┘       └─
txt                    └────┘                └┘       └─
par                    └────┘                └┘       └─
pid                                        └┘       
st                    └─────────────────────────────────
486  
src  
typ  
doc  
txt  
par  
pid  
st   
487  lemma inter_eq_Inter {s₁ s₂ : set α} : s₁ ∩ s₂ = ⋂ b : bool, cond b s₁ s₂ :=
id                                 └─┘     └┘  └┘       └──┘ └──┘  └┘ └┘
src                                └─┘                   └──┘ └──┘
typ                                └─┘     └┘  └┘       └──┘ └──┘  └┘ └┘
doc                                                            
488  set.ext $ λ x, by simp [bool.forall_bool, and_comm]
id   └─────┘                └──────────────┘  └──────┘
src  └─────┘           └────┘└──────────────┘└┘└──────┘└─
typ  └─────┘          └────┘└──────────────┘└┘└──────┘└─
doc                    └────┘                └┘        └─
txt                    └────┘                └┘        └─
par                    └────┘                └┘        └─
pid                                        └┘        
st                    └──────────────────────────────────
489  
src  
typ  
doc  
txt  
par  
pid  
st   
490  instance : complete_boolean_algebra (set α) :=
id              └──────────────────────┘  └─┘ 
src             └──────────────────────┘  └─┘
typ             └──────────────────────┘  └─┘ 
doc             └──────────────────────┘
491  { neg                 := compl,
id                            └───┘
src                           └───┘
typ                           └───┘
492    sub                 := (\),
id                            
src                           
typ                           
493    inf_neg_eq_bot      := assume s, ext $ assume x, ⟨assume ⟨h, nh⟩, nh h, false.elim⟩,
id                                     └─┘                      └┘         └────────┘
src                                     └─┘                                    └────────┘
typ                                    └─┘                      └┘         └────────┘
494    sup_neg_eq_top      := assume s, ext $ assume x, ⟨assume h, trivial, assume _, classical.em $ x ∈ s⟩,
id                                     └─┘                      └─────┘           └──────────┘     
src                                     └─┘                        └─────┘            └──────────┘     
typ                                    └─┘                      └─────┘           └──────────┘     
495    le_sup_inf          := distrib_lattice.le_sup_inf,
id                            └────────────────────────┘
src                           └────────────────────────┘
typ                           └────────────────────────┘
496    sub_eq              := assume x y, rfl,
id                                      └─┘
src                                       └─┘
typ                                     └─┘
497    infi_sup_le_sup_Inf := assume s t x, show x ∈ (⋂ b ∈ t, s ∪ b) → x ∈ s ∪ (⋂₀ t),
id                                                              └┘ 
src                                                                        └┘
typ                                                             └┘ 
doc                                                                            └┘
498      by simp; exact assume h,
src         └──┘  └────┘      └───
typ         └──┘  └────┘      └───
doc         └──┘  └────┘      └───
txt         └──┘  └────┘      └───
par         └──┘  └────┘      └───
pid                          └───
st         └──────────────────────
499        or.imp_right
id         └──────────┘
src  ─────┘└──────────┘
typ  ─────┘└──────────┘
doc  ─────┘            
txt  ─────┘            
par  ─────┘            
pid  ─────┘            
st   ───────────────────
500          (assume hn : x ∉ s, assume i hi, or.resolve_left (h i hi) hn)
id                                           └─────────────┘
src  ───────┘       └────┘  └┘      └─────┘└─────────────┘     └┘  └─
typ  ───────┘       └────┘  └┘      └─────┘└─────────────┘     └┘  └─
doc  ───────┘       └────┘   └┘      └─────┘                    └┘  └─
txt  ───────┘       └────┘   └┘      └─────┘                    └┘  └─
par  ───────┘       └────┘   └┘      └─────┘                    └┘  └─
pid  ───────┘       └────┘   └┘      └─────┘                    └┘  └─
st   ──────────────────────────────────────────────────────────────────────
501          (classical.em $ x ∈ s),
id            └──────────┘      
src  ───────┘ └──────────┘    
typ  ───────┘ └──────────┘  
doc  ───────┘                 
txt  ───────┘                 
par  ───────┘                 
pid  ───────┘                 
st   ─────────────────────────────┘
502    inf_Sup_le_supr_inf := assume s t x, show x ∈ s ∩ (⋃₀ t) → x ∈ (⋃ b ∈ t, s ∩ b),
id                                                 └┘              
src                                                     └┘                   
typ                                                └┘              
doc                                                                          
503      by simp [-and_imp, and.left_comm],
id                          └───────────┘
src         └──────────────┘└───────────┘
typ         └──────────────┘└───────────┘
doc         └──────────────┘             
txt         └──────────────┘             
par         └──────────────┘             
pid             └─────────┘             
st         └─────────────────────────────┘
504    ..set.lattice_set }
id       └─────────────┘
src      └─────────────┘
typ      └─────────────┘
505  
506  lemma sInter_union_sInter {S T : set (set α)} :
id                                    └─┘  └─┘ 
src                                   └─┘  └─┘
typ                                   └─┘  └─┘ 
507    (⋂₀S) ∪ (⋂₀T) = (⋂p ∈ set.prod S T, (p : (set α) × (set α)).1 ∪ p.2) :=
id      └┘    └┘       └──────┘        └─┘     └─┘      
src     └┘     └┘         └──────┘           └─┘      └─┘        
typ     └┘    └┘       └──────┘        └─┘     └─┘      
doc     └┘      └┘          └──────┘    
508  Inf_sup_Inf
id   └─────────┘
src  └─────────┘
typ  └─────────┘
509  
510  lemma sUnion_inter_sUnion {s t : set (set α)} :
id                                    └─┘  └─┘ 
src                                   └─┘  └─┘
typ                                   └─┘  └─┘ 
511    (⋃₀s) ∩ (⋃₀t) = (⋃p ∈ set.prod s t, (p : (set α) × (set α )).1 ∩ p.2) :=
id      └┘    └┘       └──────┘        └─┘     └─┘       
src     └┘     └┘         └──────┘           └─┘      └─┘         
typ     └┘    └┘       └──────┘        └─┘     └─┘       
doc                         └──────┘    
512  Sup_inf_Sup
id   └─────────┘
src  └─────────┘
typ  └─────────┘
513  
514  lemma sInter_bUnion {S : set (set α)} {T : set α → set (set α)} (hT : ∀s∈S, s = ⋂₀ T s) :
id                            └─┘  └─┘         └─┘    └─┘  └─┘                └┘  
src                           └─┘  └─┘          └─┘     └─┘  └─┘                    └┘
typ                           └─┘  └─┘         └─┘    └─┘  └─┘                └┘  
doc                                                                                  └┘
515    ⋂₀ (⋃s∈S, T s) = ⋂₀ S :=
id     └┘        └┘ 
src    └┘            └┘
typ    └┘        └┘ 
doc    └┘             └┘
516  begin
st   └─────
517    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
518    simp only [and_imp, exists_prop, set.mem_sInter, set.mem_Union, exists_imp_distrib],
id                └─────┘  └─────────┘  └────────────┘  └───────────┘  └────────────────┘
src    └─────────┘└─────┘└┘└─────────┘└┘└────────────┘└┘└───────────┘└┘└────────────────┘
typ    └─────────┘└─────┘└┘└─────────┘└┘└────────────┘└┘└───────────┘└┘└────────────────┘
doc    └─────────┘       └┘           └┘              └┘             └┘                  
txt    └─────────┘       └┘           └┘              └┘             └┘                  
par    └─────────┘       └┘           └┘              └┘             └┘                  
pid        └──┘└┘       └┘           └┘              └┘             └┘                  
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
519    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
520    { assume H s sS,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid      └───────────┘
st   ───┘└───────────┘└─
521      rw [hT s sS, mem_sInter],
id           └┘  └┘  └────────┘
src      └──┘     └┘└────────┘
typ      └──┘└┘└┘└┘└────────┘
doc      └──┘     └┘          
txt      └──┘     └┘          
par      └──┘     └┘          
pid        └┘     └┘          
st   ──────────────┘└──────────┘└──
522      assume t tTs,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───────────────┘└─
523      apply H t s sS tTs },
id                └┘ └─┘
src      └────┘        
typ      └────┘└┘└─┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ──────────────────────┘└┘
524    { assume H t s sS tTs,
src      └─────────────────┘
typ      └─────────────────┘
doc      └─────────────────┘
txt      └─────────────────┘
par      └─────────────────┘
pid      └─────────────────┘
st   ──────────────────────┘└─
525      have xs : x ∈ s := H s sS,
id                         └┘
src      └────────┘  └──┘  
typ      └────────┘└──┘└┘
doc      └────────┘   └──┘  
txt      └────────┘   └──┘  
par      └────────┘   └──┘  
pid      └─────┘└─┘   └──┘  
st   ────────────────────────────┘└─
526      have : s ⊆ t,
id                
src      └─────┘ 
typ      └─────┘
doc      └─────┘  
txt      └─────┘  
par      └─────┘  
pid      └───┘└┘  
st   ───────────────┘└─
527      { have Z := hT s sS,
id                   └┘  └┘
src        └────────┘   
typ        └────────┘└┘└┘
doc        └────────┘   
txt        └────────┘   
par        └────────┘   
pid        └────┘└─┘   
st   ─────┘└───────────────┘└─
528        rw sInter_eq_bInter at Z,
id            └──────────────┘
src        └─┘└──────────────┘└───┘
typ        └─┘└──────────────┘└───┘
doc        └─┘                └───┘
txt        └─┘                └───┘
par        └─┘                └───┘
pid                          └───┘
st   ─────────────────────────────┘└─
529        rw Z, apply bInter_subset_of_mem,
id                    └──────────────────┘
src        └─┘   └────┘└──────────────────┘
typ        └─┘  └────┘└──────────────────┘
doc        └─┘   └────┘
txt        └─┘   └────┘
par        └─┘   └────┘
pid                  
st   ─────────┘└──────────────────────────┘└─
530        exact tTs },
id               └─┘
src        └────┘   
typ        └────┘└─┘
doc        └────┘   
txt        └────┘   
par        └────┘   
pid                
st   ───────────────┘└┘
531      exact this xs }
id             └──┘ └┘
src      └────┘      
typ      └────┘└──┘└┘
doc      └────┘      
txt      └────┘      
par      └────┘      
pid                 
st   ─────────────────┘└─
532  end
st   ──┘
533  
534  lemma sUnion_bUnion {S : set (set α)} {T : set α → set (set α)} (hT : ∀s∈S, s = ⋃₀ T s) :
id                            └─┘  └─┘         └─┘    └─┘  └─┘                └┘  
src                           └─┘  └─┘          └─┘     └─┘  └─┘                    └┘
typ                           └─┘  └─┘         └─┘    └─┘  └─┘                └┘  
535    ⋃₀ (⋃s∈S, T s) = ⋃₀ S :=
id     └┘        └┘ 
src    └┘            └┘
typ    └┘        └┘ 
doc           
536  begin
st   └─────
537    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
538    simp only [exists_prop, set.mem_Union, set.mem_set_of_eq],
id                └─────────┘  └───────────┘  └───────────────┘
src    └─────────┘└─────────┘└┘└───────────┘└┘└───────────────┘
typ    └─────────┘└─────────┘└┘└───────────┘└┘└───────────────┘
doc    └─────────┘           └┘             └┘                 
txt    └─────────┘           └┘             └┘                 
par    └─────────┘           └┘             └┘                 
pid        └──┘└┘           └┘             └┘                 
st   ──────────────────────────────────────────────────────────┘└─
539    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
540    { rintros ⟨t, ⟨⟨s, ⟨sS, tTs⟩⟩, xt⟩⟩,
src      └───────────────────────────────┘
typ      └───────────────────────────────┘
doc      └───────────────────────────────┘
txt      └───────────────────────────────┘
par      └───────────────────────────────┘
pid             └────────────────────────┘
st   ───┘└───────────────────────────────┘└─
541      refine ⟨s, ⟨sS, _⟩⟩,
id                  └┘
src      └─────┘  └┘   └───┘
typ      └─────┘ └┘ └┘└───┘
doc      └─────┘  └┘   └───┘
txt      └─────┘  └┘   └───┘
par      └─────┘  └┘   └───┘
pid              └┘   └───┘
st   ──────────────────────┘└─
542      rw hT s sS,
id          └┘  └┘
src      └─┘   
typ      └─┘└┘└┘
doc      └─┘   
txt      └─┘   
par      └─┘   
pid           
st   ─────────────┘└─
543      exact subset_sUnion_of_mem tTs xt },
id             └──────────────────┘ └─┘ └┘
src      └────┘└──────────────────┘     
typ      └────┘└──────────────────┘└─┘└┘
doc      └────┘                         
txt      └────┘                         
par      └────┘                         
pid                                    
st   ─────────────────────────────────────┘└┘
544    { rintros ⟨s, ⟨sS, xs⟩⟩,
src      └───────────────────┘
typ      └───────────────────┘
doc      └───────────────────┘
txt      └───────────────────┘
par      └───────────────────┘
pid             └────────────┘
st   ────────────────────────┘└─
545      rw hT s sS at xs,
id          └┘  └┘
src      └─┘     └────┘
typ      └─┘└┘└┘└────┘
doc      └─┘     └────┘
txt      └─┘     └────┘
par      └─┘     └────┘
pid             └────┘
st   ───────────────────┘└─
546      rcases mem_sUnion.1 xs with ⟨t, tTs, xt⟩,
id              └────────┘   └┘
src      └─────┘└────────┘└─┘  └────────────────┘
typ      └─────┘└────────┘└─┘└┘└────────────────┘
doc      └─────┘          └─┘  └────────────────┘
txt      └─────┘          └─┘  └────────────────┘
par      └─────┘          └─┘  └────────────────┘
pid                      └─┘  └────────────────┘
st   ───────────────────────────────────────────┘└─
547      exact ⟨t, ⟨⟨s, ⟨sS, tTs⟩⟩, xt⟩⟩ }
id                     └┘  └─┘    └┘
src      └────┘  └┘   └┘   └┘   └──┘  └─┘
typ      └────┘ └┘  └┘ └┘└┘└─┘└──┘└┘└─┘
doc      └────┘  └┘   └┘   └┘   └──┘  └─┘
txt      └────┘  └┘   └┘   └┘   └──┘  └─┘
par      └────┘  └┘   └┘   └┘   └──┘  └─┘
pid             └┘   └┘   └┘   └──┘  └┘
st   ───────────────────────────────────┘└─
548  end
st   ──┘
549  
550  lemma Union_range_eq_sUnion {α β : Type*} (C : set (set α))
id                                                  └─┘  └─┘ 
src                                                 └─┘  └─┘
typ                                                 └─┘  └─┘ 
551    {f : ∀(s : C), β → s} (hf : ∀(s : C), surjective (f s)) :
id                                       └────────┘   
src                                          └────────┘
typ                                      └────────┘   
552    (⋃(y : β), range (λ(s : C), (f s y).val)) = ⋃₀ C :=
id             └───┘               └─┘     └┘ 
src             └───┘                   └─┘     └┘
typ            └───┘               └─┘     └┘ 
doc             └───┘
553  begin
st   └─────
554    ext x, split,
src    └───┘  └───┘
typ    └───┘  └───┘
doc    └───┘  └───┘
txt    └───┘  └───┘
par    └───┘  └───┘
pid       └┘
st   ──────┘└─────┘└─
555    { rintro ⟨s, ⟨y, rfl⟩, ⟨⟨s, hs⟩, rfl⟩⟩, refine ⟨_, hs, _⟩, exact (f ⟨s, hs⟩ y).2 },
id                                                        └┘                 └┘  
src      └──────────────────────────────────┘  └─────┘ └─┘  └──┘  └────┘    └┘  └┘ └──┘
typ      └──────────────────────────────────┘  └─────┘ └─┘└┘└──┘  └────┘  └┘└┘└┘└──┘
doc      └──────────────────────────────────┘  └─────┘ └─┘  └──┘  └────┘    └┘  └┘ └──┘
txt      └──────────────────────────────────┘  └─────┘ └─┘  └──┘  └────┘    └┘  └┘ └──┘
par      └──────────────────────────────────┘  └─────┘ └─┘  └──┘  └────┘    └┘  └┘ └──┘
pid            └────────────────────────────┘         └─┘  └──┘           └┘  └┘ └─┘
st   ───┘└──────────────────────────────────┘└─────────────────┘└──────────────────────┘└┘
556    { rintro ⟨s, hs, hx⟩, cases hf ⟨s, hs⟩ ⟨x, hx⟩ with y hy, refine ⟨_, ⟨y, rfl⟩, ⟨⟨s, hs⟩, _⟩⟩,
id                                 └┘    └┘     └┘                           └─┘       └┘
src      └────────────────┘  └────┘    └┘  └┘  └┘  └─────────┘  └─────┘ └─┘  └┘└─┘└─┘   └┘  └────┘
typ      └────────────────┘  └────┘└┘ └┘└┘└┘ └┘└┘└─────────┘  └─────┘ └─┘ └┘└─┘└─┘  └┘└┘└────┘
doc      └────────────────┘  └────┘    └┘  └┘  └┘  └─────────┘  └─────┘ └─┘  └┘   └─┘   └┘  └────┘
txt      └────────────────┘  └────┘    └┘  └┘  └┘  └─────────┘  └─────┘ └─┘  └┘   └─┘   └┘  └────┘
par      └────────────────┘  └────┘    └┘  └┘  └┘  └─────────┘  └─────┘ └─┘  └┘   └─┘   └┘  └────┘
pid            └──────────┘           └┘  └┘  └┘  └────────┘         └─┘  └┘   └─┘   └┘  └────┘
st   ─────────────────────┘└──────────────────────────────────┘└──────────────────────────────────┘└─
557      exact congr_arg subtype.val hy }
id             └───────┘ └─────────┘ └┘
src      └────┘└───────┘└─────────┘  
typ      └────┘└───────┘└─────────┘└┘
doc      └────┘                      
txt      └────┘                      
par      └────┘                      
pid                                 
st   ──────────────────────────────────┘└─
558  end
st   ──┘
559  
560  lemma Union_range_eq_Union {ι α β : Type*} (C : ι → set α)
id                                                      └─┘ 
src                                                      └─┘
typ                                                     └─┘ 
561    {f : ∀(x : ι), β → C x} (hf : ∀(x : ι), surjective (f x)) :
id                                        └────────┘   
src                                            └────────┘
typ                                       └────────┘   
562    (⋃(y : β), range (λ(x : ι), (f x y).val)) = ⋃x, C x :=
id             └───┘               └─┘       
src             └───┘                   └─┘      
typ            └───┘               └─┘       
doc             └───┘                             
563  begin
st   └─────
564    ext x, rw [mem_Union, mem_Union], split,
id                └───────┘  └───────┘
src    └───┘  └──┘└───────┘└┘└───────┘  └───┘
typ    └───┘  └──┘└───────┘└┘└───────┘  └───┘
doc    └───┘  └──┘         └┘           └───┘
txt    └───┘  └──┘         └┘           └───┘
par    └───┘  └──┘         └┘           └───┘
pid       └┘    └┘         └┘         
st   ──────┘└─────────────┘└─────────┘└──────┘└─
565    { rintro ⟨y, ⟨i, rfl⟩⟩, exact ⟨i, (f i y).2⟩ },
id                                          
src      └──────────────────┘  └────┘  └┘    └───┘
typ      └──────────────────┘  └────┘  └┘ └───┘
doc      └──────────────────┘  └────┘  └┘    └───┘
txt      └──────────────────┘  └────┘  └┘    └───┘
par      └──────────────────┘  └────┘  └┘    └───┘
pid            └────────────┘         └┘    └──┘
st   ───┘└──────────────────┘└─────────────────────┘└┘
566    { rintro ⟨i, hx⟩, cases hf i ⟨x, hx⟩ with y hy, refine ⟨y, ⟨i, congr_arg subtype.val hy⟩⟩ }
id                             └┘     └┘                          └───────┘ └─────────┘ └┘
src      └────────────┘  └────┘     └┘  └─────────┘  └─────┘  └┘  └┘└───────┘└─────────┘  └─┘
typ      └────────────┘  └────┘└┘ └┘└┘└─────────┘  └─────┘ └┘ └┘└───────┘└─────────┘└┘└─┘
doc      └────────────┘  └────┘     └┘  └─────────┘  └─────┘  └┘  └┘                      └─┘
txt      └────────────┘  └────┘     └┘  └─────────┘  └─────┘  └┘  └┘                      └─┘
par      └────────────┘  └────┘     └┘  └─────────┘  └─────┘  └┘  └┘                      └─┘
pid            └──────┘            └┘  └────────┘          └┘  └┘                      └┘
st   ─────────────────┘└────────────────────────────┘└──────────────────────────────────────────┘└─
567  end
st   ──┘
568  
569  @[simp] theorem sub_eq_diff (s t : set α) : s - t = s \ t := rfl
id                                      └─┘               └─┘
src                                     └─┘                    └─┘
typ                                     └─┘               └─┘
doc    └──┘
570  
571  section
572  
573  variables {p : Prop} {μ : p → set α}
id                                 └─┘
src                                └─┘
typ                                └─┘
574  
575  @[simp] lemma Inter_pos (hp : p) : (⋂h:p, μ h) = μ hp := infi_pos hp
id                                              └┘    └──────┘ └┘
src                                                        └──────┘
typ                                             └┘    └──────┘ └┘
doc    └──┘                                 
576  
577  @[simp] lemma Inter_neg (hp : ¬ p) : (⋂h:p, μ h) = univ := infi_neg hp
id                                              └──┘    └──────┘ └┘
src                                                 └──┘    └──────┘
typ                                             └──┘    └──────┘ └┘
doc    └──┘                                   
578  
579  @[simp] lemma Union_pos (hp : p) : (⋃h:p, μ h) = μ hp := supr_pos hp
id                                              └┘    └──────┘ └┘
src                                                        └──────┘
typ                                             └┘    └──────┘ └┘
doc    └──┘                                 
580  
581  @[simp] lemma Union_neg (hp : ¬ p) : (⋃h:p, μ h) = ∅ := supr_neg hp
id                                                  └──────┘ └┘
src                                                     └──────┘
typ                                                 └──────┘ └┘
doc    └──┘                                   
582  
583  @[simp] lemma Union_empty {ι : Sort*} : (⋃i:ι, ∅:set α) = ∅ := supr_bot
id                                                └─┘        └──────┘
src                                                └─┘         └──────┘
typ                                               └─┘        └──────┘
doc    └──┘                                      
584  
585  @[simp] lemma Inter_univ {ι : Sort*} : (⋂i:ι, univ:set α) = univ := infi_top
id                                              └──┘ └─┘    └──┘    └──────┘
src                                              └──┘ └─┘     └──┘    └──────┘
typ                                             └──┘ └─┘    └──┘    └──────┘
doc    └──┘                                     
586  
587  end
588  
589  section image
590  
591  lemma image_Union {f : α → β} {s : ι → set α} : f '' (⋃ i, s i) = (⋃i, f '' s i) :=
id                                       └─┘      └┘           └┘  
src                                         └─┘        └┘                └┘
typ                                      └─┘      └┘           └┘  
doc                                                                    
592  begin
st   └─────
593    apply set.ext, intro x,
id           └─────┘
src    └────┘└─────┘  └─────┘
typ    └────┘└─────┘  └─────┘
doc    └────┘         └─────┘
txt    └────┘         └─────┘
par    └────┘         └─────┘
pid                       └┘
st   ──────────────┘└───────┘└─
594    simp [image, exists_and_distrib_right.symm, -exists_and_distrib_right],
id           └───┘
src    └────┘└───┘└┘                             └──────────────────────────┘
typ    └────┘└───┘└┘└───────────────────────────┘└──────────────────────────┘
doc    └────┘     └┘                             └──────────────────────────┘
txt    └────┘     └┘                             └──────────────────────────┘
par    └────┘     └┘                             └──────────────────────────┘
pid             └┘                             └──────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
595    exact exists_swap
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ───────────────────┘
596  end
st   └─┘
597  
598  lemma univ_subtype {p : α → Prop} : (univ : set (subtype p)) = (⋃x (h : p x), {⟨x, h⟩})  :=
id                                       └──┘   └─┘  └─────┘                  
src                                       └──┘   └─┘  └─────┘                   
typ                                      └──┘   └─┘  └─────┘                  
doc                                                                             
599  set.ext $ assume ⟨x, h⟩, by simp [h]
id   └─────┘                          
src  └─────┘                     └────┘ └─
typ  └─────┘                    └────┘└─
doc                              └────┘ └─
txt                              └────┘ └─
par                              └────┘ └─
pid                                   
st                              └─────────
600  
src  
typ  
doc  
txt  
par  
pid  
st   
601  lemma range_eq_Union {ι} (f : ι → α) : range f = (⋃i, {f i}) :=
id                                        └───┘      
src                                         └───┘       
typ                                       └───┘      
doc                                         └───┘       
602  set.ext $ assume a, by simp [@eq_comm α a]
id   └─────┘                      └─────┘  
src  └─────┘                └────┘ └─────┘  └─
typ  └─────┘               └────┘ └─────┘└─
doc                         └────┘          └─
txt                         └────┘          └─
par                         └────┘          └─
pid                                       
st                         └────────────────────
603  
src  
typ  
doc  
txt  
par  
pid  
st   
604  lemma image_eq_Union (f : α → β) (s : set α) : f '' s = (⋃i∈s, {f i}) :=
id                                       └─┘      └┘       
src                                        └─┘        └┘         
typ                                      └─┘      └┘       
doc                                                              
605  set.ext $ assume b, by simp [@eq_comm β b]
id   └─────┘                      └─────┘  
src  └─────┘                └────┘ └─────┘  └─
typ  └─────┘               └────┘ └─────┘└─
doc                         └────┘          └─
txt                         └────┘          └─
par                         └────┘          └─
pid                                       
st                         └────────────────────
606  
src  
typ  
doc  
txt  
par  
pid  
st   
607  lemma bUnion_range {f : ι → α} {g : α → set β} : (⋃x ∈ range f, g x) = (⋃y, g (f y)) :=
id                                        └─┘         └───┘           
src                                          └─┘           └───┘           
typ                                       └─┘         └───┘           
doc                                                        └───┘            
608  by rw [← sUnion_image, ← range_comp, sUnion_range]
id            └──────────┘    └────────┘  └──────────┘
src     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc     └────┘            └──┘          └┘            └─
txt     └────┘            └──┘          └┘            └─
par     └────┘            └──┘          └┘            └─
pid       └──┘            └──┘          └┘            
st     └─────────────────┘└────────────┘└────────────┘
609  
src  
typ  
doc  
txt  
par  
pid  
st   
610  lemma bInter_range {f : ι → α} {g : α → set β} : (⋂x ∈ range f, g x) = (⋂y, g (f y)) :=
id                                        └─┘         └───┘           
src                                          └─┘           └───┘           
typ                                       └─┘         └───┘           
doc                                                        └───┘            
611  by rw [← sInter_image, ← range_comp, sInter_range]
id            └──────────┘    └────────┘  └──────────┘
src     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc     └────┘            └──┘          └┘            └─
txt     └────┘            └──┘          └┘            └─
par     └────┘            └──┘          └┘            └─
pid       └──┘            └──┘          └┘            
st     └─────────────────┘└────────────┘└────────────┘
612  
src  
typ  
doc  
txt  
par  
pid  
st   
613  variables {s : set γ} {f : γ → α} {g : α → set β}
id                  └─┘                         └─┘
src                 └─┘                         └─┘
typ                 └─┘                         └─┘
614  
615  lemma bUnion_image : (⋃x∈ (f '' s), g x) = (⋃y ∈ s, g (f y)) :=
id                             └┘               
src                              └┘                
typ                            └┘               
doc                                                 
616  by rw [← sUnion_image, ← image_comp, sUnion_image]
id            └──────────┘    └────────┘  └──────────┘
src     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc     └────┘            └──┘          └┘            └─
txt     └────┘            └──┘          └┘            └─
par     └────┘            └──┘          └┘            └─
pid       └──┘            └──┘          └┘            
st     └─────────────────┘└────────────┘└────────────┘
617  
src  
typ  
doc  
txt  
par  
pid  
st   
618  lemma bInter_image : (⋂x∈ (f '' s), g x) = (⋂y ∈ s, g (f y)) :=
id                             └┘               
src                              └┘                
typ                            └┘               
doc                                                 
619  by rw [← sInter_image, ← image_comp, sInter_image]
id            └──────────┘    └────────┘  └──────────┘
src     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ     └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc     └────┘            └──┘          └┘            └─
txt     └────┘            └──┘          └┘            └─
par     └────┘            └──┘          └┘            └─
pid       └──┘            └──┘          └┘            
st     └─────────────────┘└────────────┘└────────────┘
620  
src  
typ  
doc  
txt  
par  
pid  
st   
621  end image
622  
623  section preimage
624  
625  theorem monotone_preimage {f : α → β} : monotone (preimage f) := assume a b h, preimage_mono h
id                                         └──────┘  └──────┘                 └───────────┘ 
src                                          └──────┘  └──────┘                     └───────────┘
typ                                        └──────┘  └──────┘                 └───────────┘ 
doc                                          └──────┘  └──────┘
626  
627  @[simp] theorem preimage_Union {ι : Sort w} {f : α → β} {s : ι → set β} :
id                                                                 └─┘ 
src                                                                   └─┘
typ                                                                └─┘ 
doc    └──┘
628    preimage f (⋃i, s i) = (⋃i, preimage f (s i)) :=
id     └──────┘          └──────┘    
src    └──────┘               └──────┘
typ    └──────┘          └──────┘    
doc    └──────┘                └──────┘
629  set.ext $ by simp [preimage]
id   └─────┘            └──────┘
src  └─────┘      └────┘└──────┘└─
typ  └─────┘      └────┘└──────┘└─
doc               └────┘└──────┘└─
txt               └────┘        └─
par               └────┘        └─
pid                           
st               └────────────────
630  
src  
typ  
doc  
txt  
par  
pid  
st   
631  theorem preimage_bUnion {ι} {f : α → β} {s : set ι} {t : ι → set β} :
id                                              └─┘           └─┘ 
src                                               └─┘             └─┘
typ                                             └─┘           └─┘ 
632    preimage f (⋃i ∈ s, t i) = (⋃i ∈ s, preimage f (t i)) :=
id     └──────┘                └──────┘    
src    └──────┘                       └──────┘
typ    └──────┘                └──────┘    
doc    └──────┘                        └──────┘
633  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
634  
src  
typ  
doc  
txt  
par  
pid  
st   
635  @[simp] theorem preimage_sUnion {f : α → β} {s : set (set β)} :
id                                                  └─┘  └─┘ 
src                                                   └─┘  └─┘
typ                                                 └─┘  └─┘ 
doc    └──┘
636    preimage f (⋃₀ s) = (⋃t ∈ s, preimage f t) :=
id     └──────┘   └┘         └──────┘  
src    └──────┘    └┘            └──────┘
typ    └──────┘   └┘         └──────┘  
doc    └──────┘                   └──────┘
637  set.ext $ by simp [preimage]
id   └─────┘            └──────┘
src  └─────┘      └────┘└──────┘└─
typ  └─────┘      └────┘└──────┘└─
doc               └────┘└──────┘└─
txt               └────┘        └─
par               └────┘        └─
pid                           
st               └────────────────
638  
src  
typ  
doc  
txt  
par  
pid  
st   
639  lemma preimage_Inter {ι : Sort*} {s : ι → set β} {f : α → β} :
id                                            └─┘           
src                                            └─┘
typ                                           └─┘           
640    f ⁻¹' (⋂ i, s i) = (⋂ i, f ⁻¹' s i) :=
id      └─┘            └─┘  
src      └─┘                 └─┘
typ     └─┘            └─┘  
doc      └─┘                  └─┘
641  by ext; simp
src     └─┘  └────
typ     └─┘  └────
doc     └─┘  └────
txt     └─┘  └────
par     └─┘  └────
pid              
st     └──────────
642  
src  
typ  
doc  
txt  
par  
pid  
st   
643  lemma preimage_bInter {s : γ → set β} {t : set γ} {f : α → β} :
id                                 └─┘        └─┘           
src                                 └─┘         └─┘
typ                                └─┘        └─┘           
644    f ⁻¹' (⋂ i∈t, s i) = (⋂ i∈t, f ⁻¹' s i) :=
id      └─┘              └─┘  
src      └─┘                     └─┘
typ     └─┘              └─┘  
doc      └─┘                      └─┘
645  by ext; simp
src     └─┘  └────
typ     └─┘  └────
doc     └─┘  └────
txt     └─┘  └────
par     └─┘  └────
pid              
st     └──────────
646  
src  
typ  
doc  
txt  
par  
pid  
st   
647  end preimage
648  
649  
650  section seq
651  
652  def seq (s : set (α → β)) (t : set α) : set β := {b | ∃f∈s, ∃a∈t, (f : α → β) a = b}
id                └─┘             └─┘     └─┘                       
src               └─┘               └─┘      └─┘                                
typ               └─┘             └─┘     └─┘                       
653  
654  lemma seq_def {s : set (α → β)} {t : set α} : seq s t = ⋃f∈s, f '' t :=
id                      └─┘             └─┘     └─┘       └┘ 
src                     └─┘               └─┘      └─┘            └┘
typ                     └─┘             └─┘     └─┘       └┘ 
doc                                                             
655  set.ext $ by simp [seq]
id   └─────┘            └─┘
src  └─────┘      └────┘└─┘└─
typ  └─────┘      └────┘└─┘└─
doc               └────┘   └─
txt               └────┘   └─
par               └────┘   └─
pid                      
st               └───────────
656  
src  
typ  
doc  
txt  
par  
pid  
st   
657  @[simp] lemma mem_seq_iff {s : set (α → β)} {t : set α} {b : β} :
id                                  └─┘             └─┘        
src                                 └─┘               └─┘
typ                                 └─┘             └─┘        
doc    └──┘
658    b ∈ seq s t ↔ ∃ (f ∈ s) (a ∈ t), (f : α → β) a = b :=
id       └─┘                            
src       └─┘                                     
typ      └─┘                            
659  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
660  
661  lemma seq_subset {s : set (α → β)} {t : set α} {u : set β} :
id                         └─┘             └─┘        └─┘ 
src                        └─┘               └─┘         └─┘
typ                        └─┘             └─┘        └─┘ 
662    seq s t ⊆ u ↔ (∀f∈s, ∀a∈t, (f : α → β) a ∈ u) :=
id     └─┘                          
src    └─┘                                    
typ    └─┘                          
663  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
664    (assume h f hf a ha, h ⟨f, hf, a, ha, rfl⟩)
id               └┘  └┘      └┘    └┘  └─┘
src                                          └─┘
typ              └┘  └┘      └┘    └┘  └─┘
665    (assume h b ⟨f, hf, a, ha, eq⟩, eq ▸ h f hf a ha)
id                 └┘    └┘  └┘       
src                               └┘      
typ                └┘    └┘  └┘       
666  
667  lemma seq_mono {s₀ s₁ : set (α → β)} {t₀ t₁ : set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) :
id                           └─┘                 └─┘         └┘  └┘        └┘  └┘
src                          └─┘                   └─┘                           
typ                          └─┘                 └─┘         └┘  └┘        └┘  └┘
668    seq s₀ t₀ ⊆ seq s₁ t₁ :=
id     └─┘ └┘ └┘  └─┘ └┘ └┘
src    └─┘        └─┘
typ    └─┘ └┘ └┘  └─┘ └┘ └┘
669  assume b ⟨f, hf, a, ha, eq⟩, ⟨f, hs hf, a, ht ha, eq⟩
id             └┘    └┘  └┘       └┘        └┘
src                          └┘
typ            └┘    └┘  └┘       └┘        └┘
670  
671  lemma singleton_seq {f : α → β} {t : set α} : set.seq {f} t = f '' t :=
id                                      └─┘     └─────┘      └┘ 
src                                       └─┘      └─────┘         └┘
typ                                     └─┘     └─────┘      └┘ 
672  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
673  
src  
typ  
doc  
txt  
par  
pid  
st   
674  lemma seq_singleton {s : set (α → β)} {a : α} : set.seq s {a} = (λf:α→β, f a) '' s :=
id                            └─┘                 └─────┘              └┘ 
src                           └─┘                    └─────┘                     └┘
typ                           └─┘                 └─────┘              └┘ 
675  set.ext $ by simp
id   └─────┘
src  └─────┘      └────
typ  └─────┘      └────
doc               └────
txt               └────
par               └────
pid                   
st               └─────
676  
src  
typ  
doc  
txt  
par  
pid  
st   
677  lemma seq_seq {s : set (β → γ)} {t : set (α → β)} {u : set α} :
id                      └─┘             └─┘             └─┘ 
src                     └─┘               └─┘               └─┘
typ                     └─┘             └─┘             └─┘ 
678    seq s (seq t u) = seq (seq ((∘) '' s) t) u :=
id     └─┘   └─┘     └─┘  └─┘     └┘     
src    └─┘    └─┘       └─┘  └─┘     └┘
typ    └─┘   └─┘     └─┘  └─┘     └┘     
679  begin
st   └─────
680    refine set.ext (assume c, iff.intro _ _),
id            └─────┘            └───────┘
src    └─────┘└─────┘       └──┘└───────┘└───┘
typ    └─────┘└─────┘       └──┘└───────┘└───┘
doc    └─────┘              └──┘         └───┘
txt    └─────┘              └──┘         └───┘
par    └─────┘              └──┘         └───┘
pid                        └──┘         └───┘
st   ─────────────────────────────────────────┘└─
681    { rintros ⟨f, hfs, b, ⟨g, hg, a, hau, rfl⟩, rfl⟩,
src      └────────────────────────────────────────────┘
typ      └────────────────────────────────────────────┘
doc      └────────────────────────────────────────────┘
txt      └────────────────────────────────────────────┘
par      └────────────────────────────────────────────┘
pid             └─────────────────────────────────────┘
st   ───┘└────────────────────────────────────────────┘└─
682      exact ⟨f ∘ g, ⟨(∘) f, mem_image_of_mem _ hfs, g, hg, rfl⟩, a, hau, rfl⟩ },
id                           └──────────────┘   └─┘    └┘          └─┘  └─┘
src      └────┘   └┘  └─┘ └┘└──────────────┘└─┘   └┘ └┘  └┘   └─┘ └┘   └┘└─┘└┘
typ      └────┘   └┘  └─┘└┘└──────────────┘└─┘└─┘└┘└┘└┘└┘   └─┘└┘└─┘└┘└─┘└┘
doc      └────┘    └┘  └─┘ └┘                └─┘   └┘ └┘  └┘   └─┘ └┘   └┘   └┘
txt      └────┘    └┘  └─┘ └┘                └─┘   └┘ └┘  └┘   └─┘ └┘   └┘   └┘
par      └────┘    └┘  └─┘ └┘                └─┘   └┘ └┘  └┘   └─┘ └┘   └┘   └┘
pid               └┘  └─┘ └┘                └─┘   └┘ └┘  └┘   └─┘ └┘   └┘   
st   ───────────────────────────────────────────────────────────────────────────┘└┘
683    { rintros ⟨fg, ⟨fc, ⟨f, hfs, rfl⟩, g, hgt, rfl⟩, a, ha, rfl⟩,
src      └────────────────────────────────────────────────────────┘
typ      └────────────────────────────────────────────────────────┘
doc      └────────────────────────────────────────────────────────┘
txt      └────────────────────────────────────────────────────────┘
par      └────────────────────────────────────────────────────────┘
pid             └─────────────────────────────────────────────────┘
st   ─────────────────────────────────────────────────────────────┘└─
684      exact ⟨f, hfs, g a, ⟨g, hgt, a, ha, rfl⟩, rfl⟩ }
id                └─┘          └─┘    └┘        └─┘
src      └────┘  └┘   └┘  └┘  └┘   └┘ └┘  └┘   └─┘└─┘└┘
typ      └────┘ └┘└─┘└┘  └┘ └┘└─┘└┘└┘└┘└┘   └─┘└─┘└┘
doc      └────┘  └┘   └┘  └┘  └┘   └┘ └┘  └┘   └─┘   └┘
txt      └────┘  └┘   └┘  └┘  └┘   └┘ └┘  └┘   └─┘   └┘
par      └────┘  └┘   └┘  └┘  └┘   └┘ └┘  └┘   └─┘   └┘
pid             └┘   └┘  └┘  └┘   └┘ └┘  └┘   └─┘   
st   ──────────────────────────────────────────────────┘└─
685  end
st   ──┘
686  
687  lemma image_seq {f : β → γ} {s : set (α → β)} {t : set α} :
id                                  └─┘             └─┘ 
src                                   └─┘               └─┘
typ                                 └─┘             └─┘ 
688    f '' seq s t = seq ((∘) f '' s) t :=
id      └┘ └─┘    └─┘      └┘   
src      └┘ └─┘      └─┘       └┘
typ     └┘ └─┘    └─┘      └┘   
689  by rw [← singleton_seq, ← singleton_seq, seq_seq, image_singleton]
id            └───────────┘    └───────────┘  └─────┘  └─────────────┘
src     └────┘└───────────┘└──┘└───────────┘└┘└─────┘└┘└─────────────┘└─
typ     └────┘└───────────┘└──┘└───────────┘└┘└─────┘└┘└─────────────┘└─
doc     └────┘             └──┘             └┘       └┘               └─
txt     └────┘             └──┘             └┘       └┘               └─
par     └────┘             └──┘             └┘       └┘               └─
pid       └──┘             └──┘             └┘       └┘               
st     └──────────────────┘└───────────────┘└───────┘└───────────────┘
690  
src  
typ  
doc  
txt  
par  
pid  
st   
691  lemma prod_eq_seq {s : set α} {t : set β} : set.prod s t = (prod.mk '' s).seq t :=
id                          └─┘        └─┘     └──────┘     └─────┘ └┘  └─┘  
src                         └─┘         └─┘      └──────┘       └─────┘ └┘   └─┘
typ                         └─┘        └─┘     └──────┘     └─────┘ └┘  └─┘  
doc                                              └──────┘
692  begin
st   └─────
693    ext ⟨a, b⟩,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid       └─────┘
st   ───────────┘└─
694    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
695    { rintros ⟨ha, hb⟩, exact ⟨prod.mk a, ⟨a, ha, rfl⟩, b, hb, rfl⟩ },
id                                └─────┘       └┘          └┘  └─┘
src      └──────────────┘  └────┘ └─────┘ └┘  └┘  └┘   └─┘ └┘  └┘└─┘└┘
typ      └──────────────┘  └────┘ └─────┘ └┘ └┘└┘└┘   └─┘└┘└┘└┘└─┘└┘
doc      └──────────────┘  └────┘         └┘  └┘  └┘   └─┘ └┘  └┘   └┘
txt      └──────────────┘  └────┘         └┘  └┘  └┘   └─┘ └┘  └┘   └┘
par      └──────────────┘  └────┘         └┘  └┘  └┘   └─┘ └┘  └┘   └┘
pid             └───────┘                └┘  └┘  └┘   └─┘ └┘  └┘   
st   ───┘└──────────────┘└────────────────────────────────────────────┘└┘
696    { rintros ⟨f, ⟨x, hx, rfl⟩, y, hy, eq⟩, rw ← eq, exact ⟨hx, hy⟩ }
id                                                  └┘         └┘  └┘
src      └──────────────────────────────────┘  └───┘└┘  └────┘   └┘  └┘
typ      └──────────────────────────────────┘  └───┘└┘  └────┘ └┘└┘└┘└┘
doc      └──────────────────────────────────┘  └───┘    └────┘   └┘  └┘
txt      └──────────────────────────────────┘  └───┘    └────┘   └┘  └┘
par      └──────────────────────────────────┘  └───┘    └────┘   └┘  └┘
pid             └───────────────────────────┘    └─┘            └┘  
st   ───────────────────────────────────────┘└───────┘└───────────────┘└─
697  end
st   ──┘
698  
699  lemma prod_image_seq_comm (s : set α) (t : set β) :
id                                  └─┘        └─┘ 
src                                 └─┘         └─┘
typ                                 └─┘        └─┘ 
700    (prod.mk '' s).seq t = seq ((λb a, (a, b)) '' t) s :=
id      └─────┘ └┘  └─┘    └─┘            └┘   
src     └─────┘ └┘   └─┘     └─┘                └┘
typ     └─────┘ └┘  └─┘    └─┘            └┘   
701  by rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]
id            └─────────┘    └─────────────┘  └─────────┘  └───────┘    └────────┘
src     └────┘└─────────┘└──┘└─────────────┘└┘└─────────┘└┘└───────┘└──┘└────────┘└─
typ     └────┘└─────────┘└──┘└─────────────┘└┘└─────────┘└┘└───────┘└──┘└────────┘└─
doc     └────┘           └──┘               └┘           └┘         └──┘          └─
txt     └────┘           └──┘               └┘           └┘         └──┘          └─
par     └────┘           └──┘               └┘           └┘         └──┘          └─
pid       └──┘           └──┘               └┘           └┘         └──┘          
st     └────────────────┘└─────────────────┘└───────────┘└─────────┘└────────────┘
702  
src  
typ  
doc  
txt  
par  
pid  
st   
703  end seq
704  
705  theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
id                          └──────┘           └─┘           └─┘ 
src                         └──────┘             └─┘             └─┘
typ                         └──────┘           └─┘           └─┘ 
706    (hf : monotone f) (hg : monotone g) : monotone (λx, set.prod (f x) (g x)) :=
id           └──────┘         └──────┘     └──────┘     └──────┘       
src          └──────┘          └──────┘      └──────┘      └──────┘
typ          └──────┘         └──────┘     └──────┘     └──────┘       
doc          └──────┘          └──────┘      └──────┘      └──────┘
707  assume a b h, prod_mono (hf h) (hg h)
id              └───────┘  └┘    └┘ 
src                └───────┘
typ             └───────┘  └┘    └┘ 
708  
709  instance : monad set :=
id              └───┘ └─┘
src             └───┘ └─┘
typ             └───┘ └─┘
710  { pure       := λ(α : Type u) a, {a},
id                         └──┘      
src                                   
typ                        └──┘      
711    bind       := λ(α β : Type u) s f, ⋃i∈s, f i,
id                           └──┘          
src                                          
typ                          └──┘          
doc                                          
712    seq        := λ(α β : Type u), set.seq,
id                           └──┘     └─────┘
src                                   └─────┘
typ                          └──┘     └─────┘
713    map        := λ(α β : Type u), set.image }
id                           └──┘     └───────┘
src                                   └───────┘
typ                          └──┘     └───────┘
714  
715  instance : is_lawful_monad set :=
id              └─────────────┘ └─┘
src             └─────────────┘ └─┘
typ             └─────────────┘ └─┘
716  { pure_bind             := assume α β x f, by simp,
id                                       
src                                               └──┘
typ                                           └──┘
doc                                                └──┘
txt                                                └──┘
par                                                └──┘
st                                                └───┘
717    bind_assoc            := assume α β γ s f g, set.ext $ assume a,
id                                            └─────┘          
src                                                 └─────┘
typ                                           └─────┘          
718      by simp [exists_and_distrib_right.symm, -exists_and_distrib_right,
src         └────┘                             └────────────────────────────
typ         └────┘└───────────────────────────┘└────────────────────────────
doc         └────┘                             └────────────────────────────
txt         └────┘                             └────────────────────────────
par         └────┘                             └────────────────────────────
pid                                          └────────────────────────────
st         └────────────────────────────────────────────────────────────────
719               exists_and_distrib_left.symm, -exists_and_distrib_left, and_assoc];
id                                                                        └───────┘
src  ────────────┘                            └──────────────────────────┘└───────┘
typ  ────────────┘└──────────────────────────┘└──────────────────────────┘└───────┘
doc  ────────────┘                            └──────────────────────────┘         
txt  ────────────┘                            └──────────────────────────┘         
par  ────────────┘                            └──────────────────────────┘         
pid  ────────────┘                            └──────────────────────────┘         
st   ─────────────────────────────────────────────────────────────────────────────────
720         exact exists_swap,
id                └─────────┘
src         └────┘└─────────┘
typ         └────┘└─────────┘
doc         └────┘
txt         └────┘
par         └────┘
pid              
st   ───────────────────────┘
721    id_map                := assume α, id_map,
id                                       └────┘
src                                       └────┘
typ                                      └────┘
722    bind_pure_comp_eq_map := assume α β f s, set.ext $ by simp [set.image, eq_comm],
id                                          └─────┘            └───────┘  └─────┘
src                                             └─────┘      └────┘└───────┘└┘└─────┘
typ                                         └─────┘      └────┘└───────┘└┘└─────┘
doc                                                          └────┘         └┘       
txt                                                          └────┘         └┘       
par                                                          └────┘         └┘       
pid                                                                       └┘       
st                                                          └────────────────────────┘
723    bind_map_eq_seq       := assume α β s t, by simp [seq_def] }
id                                                   └─────┘
src                                                └────┘└─────┘└┘
typ                                            └────┘└─────┘└┘
doc                                                └────┘       └┘
txt                                                └────┘       └┘
par                                                └────┘       └┘
pid                                                           
st                                                └──────────────┘
724  
725  instance : is_comm_applicative (set : Type u → Type u) :=
id              └─────────────────┘  └─┘   └──┘
src             └─────────────────┘  └─┘
typ             └─────────────────┘  └─┘   └──┘
726  ⟨ assume α β s t, prod_image_seq_comm s t ⟩
id                 └─────────────────┘  
src                    └─────────────────┘
typ                └─────────────────┘  
727  
728  section monad
729  variables {α' β' : Type u} {s : set α'} {f : α' → set β'} {g : set (α' → β')}
id                                   └─┘               └─┘          └─┘
src                                  └─┘               └─┘          └─┘
typ                                  └─┘               └─┘          └─┘
730  
731  @[simp] lemma bind_def : s >>= f = ⋃i∈s, f i := rfl
id                             └─┘          └─┘
src                             └─┘               └─┘
typ                            └─┘          └─┘
doc    └──┘                                
732  
733  @[simp] lemma fmap_eq_image (f : α' → β') : f <$> s = f '' s := rfl
id                                    └┘   └┘     └─┘    └┘     └─┘
src                                                └─┘      └┘      └─┘
typ                                   └┘   └┘     └─┘    └┘     └─┘
doc    └──┘
734  
735  @[simp] lemma seq_eq_set_seq {α β : Type*} (s : set (α → β)) (t : set α) : s <*> t = s.seq t := rfl
id                                                   └─┘             └─┘      └─┘   └──┘     └─┘
src                                                  └─┘               └─┘        └─┘     └──┘      └─┘
typ                                                  └─┘             └─┘      └─┘   └──┘     └─┘
doc    └──┘
736  
737  @[simp] lemma pure_def (a : α) : (pure a : set α) = {a} := rfl
id                                    └──┘    └─┘         └─┘
src                                    └──┘     └─┘           └─┘
typ                                   └──┘    └─┘         └─┘
doc    └──┘
738  
739  end monad
740  
741  section pi
742  
743  lemma pi_def {α : Type*} {π : α → Type*} (i : set α) (s : Πa, set (π a)) :
id                                                └─┘           └─┘   
src                                                └─┘             └─┘
typ                                               └─┘           └─┘   
744    pi i s = (⋂ a∈i, ((λf:(Πa, π a), f a) ⁻¹' (s a))) :=
id     └┘                        └─┘   
src    └┘                                 └─┘
typ    └┘                        └─┘   
doc    └┘                                  └─┘
745  by ext; simp [pi]
id                 └┘
src     └─┘  └────┘└┘└─
typ     └─┘  └────┘└┘└─
doc     └─┘  └────┘└┘└─
txt     └─┘  └────┘  └─
par     └─┘  └────┘  └─
pid                
st     └───────────────
746  
src  
typ  
doc  
txt  
par  
pid  
st   
747  end pi
748  
749  end set
750  
751  /- disjoint sets -/
752  
753  section disjoint
754  variable [semilattice_inf_bot α]
id             └─────────────────┘
src            └─────────────────┘
typ            └─────────────────┘
doc            └─────────────────┘
755  
756  /-- Two elements of a lattice are disjoint if their inf is the bottom element.
757    (This generalizes disjoint sets, viewed as members of the subset lattice.) -/
758  def disjoint (a b : α) : Prop := a ⊓ b ≤ ⊥
id                                       
src                                         
typ                                      
759  
760  theorem disjoint.eq_bot {a b : α} (h : disjoint a b) : a ⊓ b = ⊥ :=
id                                         └──────┘          
src                                         └──────┘              
typ                                        └──────┘          
doc                                         └──────┘
761  eq_bot_iff.2 h
id   └────────┘  
src  └────────┘
typ  └────────┘  
762  
763  theorem disjoint_iff {a b : α} : disjoint a b ↔ a ⊓ b = ⊥ :=
id                                   └──────┘        
src                                   └──────┘            
typ                                  └──────┘        
doc                                   └──────┘
764  eq_bot_iff.symm
id   └────────┘└───┘
src  └────────┘└───┘
typ  └────────┘└───┘
765  
766  theorem disjoint.comm {a b : α} : disjoint a b ↔ disjoint b a :=
id                                    └──────┘    └──────┘  
src                                    └──────┘      └──────┘
typ                                   └──────┘    └──────┘  
doc                                    └──────┘       └──────┘
767  by rw [disjoint, disjoint, inf_comm]
id          └──────┘  └──────┘  └──────┘
src     └──┘└──────┘└┘└──────┘└┘└──────┘└─
typ     └──┘└──────┘└┘└──────┘└┘└──────┘└─
doc     └──┘└──────┘└┘└──────┘└┘        └─
txt     └──┘        └┘        └┘        └─
par     └──┘        └┘        └┘        └─
pid       └┘        └┘        └┘        
st     └───────────┘└────────┘└────────┘
768  
src  
typ  
doc  
txt  
par  
pid  
st   
769  theorem disjoint.symm {a b : α} : disjoint a b → disjoint b a :=
id                                    └──────┘     └──────┘  
src                                    └──────┘       └──────┘
typ                                   └──────┘     └──────┘  
doc                                    └──────┘       └──────┘
770  disjoint.comm.1
id   └───────────┘
src  └───────────┘
typ  └───────────┘
771  
772  @[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := disjoint_iff.2 bot_inf_eq
id                                              └──────┘      └──────────┘  └────────┘
src                                              └──────┘       └──────────┘  └────────┘
typ                                             └──────┘      └──────────┘  └────────┘
doc    └──┘                                      └──────┘
773  @[simp] theorem disjoint_bot_right {a : α} : disjoint a ⊥ := disjoint_iff.2 inf_bot_eq
id                                               └──────┘      └──────────┘  └────────┘
src                                               └──────┘       └──────────┘  └────────┘
typ                                              └──────┘      └──────────┘  └────────┘
doc    └──┘                                       └──────┘
774  
775  theorem disjoint_mono {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
id                                                        
src                                                          
typ                                                       
776    disjoint b d → disjoint a c := le_trans (inf_le_inf h₁ h₂)
id     └──────┘     └──────┘      └──────┘  └────────┘ └┘ └┘
src    └──────┘       └──────┘        └──────┘  └────────┘
typ    └──────┘     └──────┘      └──────┘  └────────┘ └┘ └┘
doc    └──────┘       └──────┘
777  
778  theorem disjoint_mono_left {a b c : α} (h : a ≤ b) : disjoint b c → disjoint a c :=
id                                                    └──────┘     └──────┘  
src                                                      └──────┘       └──────┘
typ                                                   └──────┘     └──────┘  
doc                                                       └──────┘       └──────┘
779  disjoint_mono h (le_refl _)
id   └───────────┘   └─────┘
src  └───────────┘    └─────┘
typ  └───────────┘   └─────┘
780  
781  theorem disjoint_mono_right {a b c : α} (h : b ≤ c) : disjoint a c → disjoint a b :=
id                                                     └──────┘     └──────┘  
src                                                       └──────┘       └──────┘
typ                                                    └──────┘     └──────┘  
doc                                                        └──────┘       └──────┘
782  disjoint_mono (le_refl _) h
id   └───────────┘  └─────┘    
src  └───────────┘  └─────┘
typ  └───────────┘  └─────┘    
783  
784  @[simp] lemma disjoint_self {a : α} : disjoint a a ↔ a = ⊥ :=
id                                        └──────┘      
src                                        └──────┘         
typ                                       └──────┘      
doc    └──┘                                └──────┘
785  by simp [disjoint]
id            └──────┘
src     └────┘└──────┘└─
typ     └────┘└──────┘└─
doc     └────┘└──────┘└─
txt     └────┘        └─
par     └────┘        └─
pid                 
st     └────────────────
786  
src  
typ  
doc  
txt  
par  
pid  
st   
787  lemma ne_of_disjoint {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) : a ≠ b :=
id                                                  └──────┘        
src                                                   └──────┘          
typ                                                 └──────┘        
doc                                                     └──────┘
788  by { intro h, rw [←h, disjoint_self] at hab, exact ha hab }
id                        └───────────┘                └┘ └─┘
src       └─────┘  └───┘ └┘└───────────┘└──────┘  └────┘     
typ       └─────┘  └───┘└┘└───────────┘└──────┘  └────┘└┘└─┘
doc       └─────┘  └───┘ └┘             └──────┘  └────┘     
txt       └─────┘  └───┘ └┘             └──────┘  └────┘     
par       └─────┘  └───┘ └┘             └──────┘  └────┘     
pid            └┘    └─┘ └┘             └─────┘            
st     └────────┘└──────┘└─────────────┘└─────┘└─────────────┘└┘
789  
790  end disjoint
791  
792  namespace set
793  
794  protected theorem disjoint_iff {s t : set α} : disjoint s t ↔ s ∩ t ⊆ ∅ := iff.rfl
id                                         └─┘     └──────┘            └─────┘
src                                        └─┘      └──────┘                └─────┘
typ                                        └─┘     └──────┘            └─────┘
doc                                                 └──────┘
795  
796  lemma not_disjoint_iff {s t : set α} : ¬disjoint s t ↔ ∃x, x ∈ s ∧ x ∈ t :=
id                                 └─┘     └──────┘           
src                                └─┘      └──────┘                
typ                                └─┘     └──────┘           
doc                                          └──────┘
797  (not_congr (set.disjoint_iff.trans subset_empty_iff)).trans ne_empty_iff_nonempty
id    └───────┘  └──────────────┘└────┘ └──────────────┘  └───┘  └───────────────────┘
src   └───────┘  └──────────────┘└────┘ └──────────────┘  └───┘  └───────────────────┘
typ   └───────┘  └──────────────┘└────┘ └──────────────┘  └───┘  └───────────────────┘
798  
799  lemma disjoint_left {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
id                              └─┘     └──────┘                 
src                             └─┘      └──────┘                      
typ                             └─┘     └──────┘                 
doc                                      └──────┘
800  show (∀ x, ¬(x ∈ s ∩ t)) ↔ _, from ⟨λ h a, not_and.1 $ h a, λ h a, not_and.2 $ h a⟩
id                                    └─────┘            └─────┘     
src                                         └─────┘                └─────┘
typ                                   └─────┘            └─────┘     
801  
802  theorem disjoint_right {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s :=
id                                 └─┘     └──────┘                 
src                                └─┘      └──────┘                      
typ                                └─┘     └──────┘                 
doc                                         └──────┘
803  by rw [disjoint.comm, disjoint_left]
id          └───────────┘  └───────────┘
src     └──┘└───────────┘└┘└───────────┘└─
typ     └──┘└───────────┘└┘└───────────┘└─
doc     └──┘             └┘             └─
txt     └──┘             └┘             └─
par     └──┘             └┘             └─
pid       └┘             └┘             
st     └────────────────┘└─────────────┘
804  
src  
typ  
doc  
txt  
par  
pid  
st   
805  theorem disjoint_diff {a b : set α} : disjoint a (b \ a) :=
id                                └─┘     └──────┘     
src                               └─┘      └──────┘      
typ                               └─┘     └──────┘     
doc                                        └──────┘
806  disjoint_iff.2 (inter_diff_self _ _)
id   └──────────┘   └─────────────┘
src  └──────────┘   └─────────────┘
typ  └──────────┘   └─────────────┘
807  
808  theorem disjoint_compl (s : set α) : disjoint s (-s) := assume a ⟨h₁, h₂⟩, h₂ h₁
id                               └─┘     └──────┘                └┘  └┘
src                              └─┘      └──────┘    
typ                              └─┘     └──────┘                └┘  └┘
doc                                       └──────┘
809  
810  theorem disjoint_singleton_left {a : α} {s : set α} : disjoint {a} s ↔ a ∉ s :=
id                                               └─┘     └──────┘       
src                                               └─┘      └──────┘         
typ                                              └─┘     └──────┘       
doc                                                        └──────┘
811  by simp [set.disjoint_iff, subset_def]; exact iff.rfl
id            └──────────────┘  └────────┘         └─────┘
src     └────┘└──────────────┘└┘└────────┘  └────┘└─────┘
typ     └────┘└──────────────┘└┘└────────┘  └────┘└─────┘
doc     └────┘                └┘            └────┘       
txt     └────┘                └┘            └────┘       
par     └────┘                └┘            └────┘       
pid                         └┘                        
st     └───────────────────────────────────────────────────
812  
src  
typ  
doc  
txt  
par  
pid  
st   
813  theorem disjoint_singleton_right {a : α} {s : set α} : disjoint s {a} ↔ a ∉ s :=
id                                                └─┘     └──────┘       
src                                                └─┘      └──────┘         
typ                                               └─┘     └──────┘       
doc                                                         └──────┘
814  by rw [disjoint.comm]; exact disjoint_singleton_left
id          └───────────┘         └─────────────────────┘
src     └──┘└───────────┘  └────┘└─────────────────────┘
typ     └──┘└───────────┘  └────┘└─────────────────────┘
doc     └──┘               └────┘                       
txt     └──┘               └────┘                       
par     └──┘               └────┘                       
pid       └┘                                           
st     └────────────────┘└───────────────────────────────
815  
src  
typ  
doc  
txt  
par  
pid  
st   
816  theorem disjoint_image_image {f : β → α} {g : γ → α} {s : set β} {t : set γ}
id                                                         └─┘        └─┘ 
src                                                            └─┘         └─┘
typ                                                        └─┘        └─┘ 
817    (h : ∀b∈s, ∀c∈t, f b ≠ g c) : disjoint (f '' s) (g '' t) :=
id                          └──────┘   └┘     └┘ 
src                                 └──────┘    └┘       └┘
typ                         └──────┘   └┘     └┘ 
doc                                  └──────┘
818  by rintros a ⟨⟨b, hb, eq⟩, ⟨c, hc, rfl⟩⟩; exact h b hb c hc eq
id                                                     └┘  └┘ └┘
src     └───────────────────────────────────┘  └────┘       └┘
typ     └───────────────────────────────────┘  └────┘└┘└┘└┘
doc     └───────────────────────────────────┘  └────┘         
txt     └───────────────────────────────────┘  └────┘         
par     └───────────────────────────────────┘  └────┘         
pid            └────────────────────────────┘                
st     └────────────────────────────────────────────────────────────
819  
src  
typ  
doc  
txt  
par  
pid  
st   
820  def pairwise_disjoint (s : set (set α)) : Prop :=
id                              └─┘  └─┘ 
src                             └─┘  └─┘
typ                             └─┘  └─┘ 
821  pairwise_on s disjoint
id   └─────────┘  └──────┘
src  └─────────┘   └──────┘
typ  └─────────┘  └──────┘
doc  └─────────┘   └──────┘
822  
823  lemma pairwise_disjoint_subset {s t : set (set α)} (h : s ⊆ t)
id                                         └─┘  └─┘           
src                                        └─┘  └─┘            
typ                                        └─┘  └─┘           
824    (ht : pairwise_disjoint t) : pairwise_disjoint s :=
id           └───────────────┘     └───────────────┘ 
src          └───────────────┘      └───────────────┘
typ          └───────────────┘     └───────────────┘ 
825  pairwise_on.mono h ht
id   └──────────────┘  └┘
src  └──────────────┘
typ  └──────────────┘  └┘
826  
827  lemma pairwise_disjoint_range {s : set (set α)} (f : s → set α) (hf : ∀(x : s), f x ⊆ x.1)
id                                      └─┘  └─┘            └─┘                     
src                                     └─┘  └─┘              └─┘                          
typ                                     └─┘  └─┘            └─┘                     
828    (ht : pairwise_disjoint s) : pairwise_disjoint (range f) :=
id           └───────────────┘     └───────────────┘  └───┘ 
src          └───────────────┘      └───────────────┘  └───┘
typ          └───────────────┘     └───────────────┘  └───┘ 
doc                                                    └───┘
829  begin
st   └─────
830    rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy, refine disjoint_mono (hf x) (hf y) (ht _ x.2 _ y.2 _),
id                                              └───────────┘         └┘     └┘        
src    └──────────────────────────────┘  └─────┘└───────────┘    └┘    └┘   └─┘ └───┘ └───┘
typ    └──────────────────────────────┘  └─────┘└───────────┘    └┘ └┘ └┘ └┘└─┘└───┘└───┘
doc    └──────────────────────────────┘  └─────┘                 └┘    └┘   └─┘ └───┘ └───┘
txt    └──────────────────────────────┘  └─────┘                 └┘    └┘   └─┘ └───┘ └───┘
par    └──────────────────────────────┘  └─────┘                 └┘    └┘   └─┘ └───┘ └───┘
pid          └────────────────────────┘                         └┘    └┘   └─┘ └───┘ └───┘
st   ─────────────────────────────────┘└─────────────────────────────────────────────────────┘└─
831    intro h, apply hxy, apply congr_arg f, exact subtype.eq h
id                               └───────┘         └────────┘ 
src    └─────┘  └────┘     └────┘└───────┘   └────┘└────────┘ 
typ    └─────┘  └────┘     └────┘└───────┘  └────┘└────────┘
doc    └─────┘  └────┘     └────┘            └────┘           
txt    └─────┘  └────┘     └────┘            └────┘           
par    └─────┘  └────┘     └────┘            └────┘           
pid         └┘                                             
st   ────────┘└─────────┘└─────────────────┘└───────────────────┘
832  end
st   └─┘
833  
834  /- warning: classical -/
835  lemma pairwise_disjoint_elim {s : set (set α)} (h : pairwise_disjoint s) {x y : set α}
id                                     └─┘  └─┘         └───────────────┘          └─┘ 
src                                    └─┘  └─┘          └───────────────┘           └─┘
typ                                    └─┘  └─┘         └───────────────┘          └─┘ 
836    (hx : x ∈ s) (hy : y ∈ s) (z : α) (hzx : z ∈ x) (hzy : z ∈ y) : x = y :=
id                                                          
src                                                                  
typ                                                         
837  classical.not_not.1 $ λ h', h x hx y hy h' ⟨hzx, hzy⟩
id   └───────────────┘      └┘    └┘  └┘ └┘  └─┘  └─┘
src  └───────────────┘
typ  └───────────────┘      └┘    └┘  └┘ └┘  └─┘  └─┘
838  
839  end set
840  
841  namespace set
842  variables (t : α → set β)
id                      └─┘
src                     └─┘
typ                     └─┘
843  
844  def sigma_to_Union (x : Σi, t i) : (⋃i, t i) := ⟨x.2, mem_Union.2 ⟨x.1, x.2.2⟩⟩
id                                             └───────┘       
src                                                   └───────┘         
typ                                            └───────┘       
doc                                       
845  
846  lemma surjective_sigma_to_Union : surjective (sigma_to_Union t)
id                                     └────────┘  └────────────┘ 
src                                    └────────┘  └────────────┘
typ                                    └────────┘  └────────────┘ 
847  | ⟨b, hb⟩ := have ∃a, b ∈ t a, by simpa using hb, let ⟨a, hb⟩ := this in ⟨⟨a, ⟨b, hb⟩⟩, rfl⟩
id                                          └┘  └─┘    └┘     └──┘                   └─┘
src                                 └──────────┘                                          └─┘
typ                             └──────────┘└┘  └─┘    └┘     └──┘                   └─┘
doc                                    └──────────┘
txt                                    └──────────┘
par                                    └──────────┘
pid                                         └────┘
st                                    └─────────────┘
848  
849  lemma injective_sigma_to_Union (h : ∀i j, i ≠ j → disjoint (t i) (t j)) :
id                                                └──────┘       
src                                                   └──────┘
typ                                               └──────┘       
doc                                                    └──────┘
850    injective (sigma_to_Union t)
id     └───────┘  └────────────┘ 
src    └───────┘  └────────────┘
typ    └───────┘  └────────────┘ 
851  | ⟨a₁, ⟨b₁, h₁⟩⟩ ⟨a₂, ⟨b₂, h₂⟩⟩ eq :=
id      └┘   └┘  └┘    └┘   └┘  └┘   └┘
src                                  └┘
typ     └┘   └┘  └┘    └┘   └┘  └┘   └┘
852    have b_eq : b₁ = b₂, from congr_arg subtype.val eq,
id                              └───────┘ └─────────┘
src                             └───────┘ └─────────┘
typ                             └───────┘ └─────────┘
853    have a_eq : a₁ = a₂, from classical.by_contradiction $ assume ne,
id                              └────────────────────────┘          └┘
src                             └────────────────────────┘          └┘
typ                             └────────────────────────┘          └┘
854      have b₁ ∈ t a₁ ∩ t a₂, from ⟨h₁, b_eq.symm ▸ h₂⟩,
id                                    └──┘└───┘ 
src                                         └───┘ 
typ                                   └──┘└───┘ 
855      h _ _ ne this,
id            └┘ └──┘
src            └┘
typ           └┘ └──┘
856    sigma.eq a_eq $ subtype.eq $ by subst b_eq; subst a_eq
id     └──────┘ └──┘   └────────┘            └──┘        └──┘
src    └──────┘        └────────┘      └────┘      └────┘    
typ    └──────┘ └──┘   └────────┘      └────┘└──┘  └────┘└──┘
doc                                    └────┘      └────┘    
txt                                    └────┘      └────┘    
par                                    └────┘      └────┘    
pid                                                        
st                                    └───────────────────────
857  
src  
typ  
doc  
txt  
par  
pid  
st   
858  lemma bijective_sigma_to_Union (h : ∀i j, i ≠ j → disjoint (t i) (t j)) :
id                                                └──────┘       
src                                                   └──────┘
typ                                               └──────┘       
doc                                                    └──────┘
859    bijective (sigma_to_Union t) :=
id     └───────┘  └────────────┘ 
src    └───────┘  └────────────┘
typ    └───────┘  └────────────┘ 
860  ⟨injective_sigma_to_Union t h, surjective_sigma_to_Union t⟩
id    └──────────────────────┘    └───────────────────────┘ 
src   └──────────────────────┘      └───────────────────────┘
typ   └──────────────────────┘    └───────────────────────┘ 
861  
862  noncomputable def Union_eq_sigma_of_disjoint {t : α → set β}
id                                                        └─┘ 
src                                                        └─┘
typ                                                       └─┘ 
863    (h : ∀i j, i ≠ j → disjoint (t i) (t j)) : (⋃i, t i) ≃ (Σi, t i) :=
id                   └──────┘                     
src                      └──────┘                           
typ                  └──────┘                     
doc                       └──────┘                        
864  (equiv.of_bijective $ bijective_sigma_to_Union t h).symm
id    └────────────────┘   └──────────────────────┘   └──┘
src   └────────────────┘   └──────────────────────┘     └──┘
typ   └────────────────┘   └──────────────────────┘   └──┘
865  
866  noncomputable def bUnion_eq_sigma_of_disjoint {s : set α} {t : α → set β}
id                                                      └─┘           └─┘ 
src                                                     └─┘             └─┘
typ                                                     └─┘           └─┘ 
867    (h : pairwise_on s (disjoint on t)) : (⋃i∈s, t i) ≃ (Σi:s, t i.val) :=
id          └─────────┘   └──────┘ └┘                  └──┘
src         └─────────┘    └──────┘ └┘                          └──┘
typ         └─────────┘   └──────┘ └┘                  └──┘
doc         └─────────┘    └──────┘                    
868  equiv.trans (equiv.set_congr (bUnion_eq_Union _ _)) $ Union_eq_sigma_of_disjoint $
id   └─────────┘  └─────────────┘  └─────────────┘         └────────────────────────┘
src  └─────────┘  └─────────────┘  └─────────────┘         └────────────────────────┘
typ  └─────────┘  └─────────────┘  └─────────────┘         └────────────────────────┘
869    assume ⟨i, hi⟩ ⟨j, hj⟩ ne, h _ hi _ hj $ assume eq, ne $ subtype.eq eq
id               └┘     └┘  └┘                      └┘  └┘   └────────┘ └┘
src                           └┘                       └┘  └┘   └────────┘ └┘
typ              └┘     └┘  └┘                      └┘  └┘   └────────┘ └┘
870  
871  end set